Last active
June 21, 2018 10:12
-
-
Save quicquid/4cd68be397ff2c7f2286e29acf3ae4fd to your computer and use it in GitHub Desktop.
cvc4 linking problem
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
only there to have a better name in the overview |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <cvc4/cvc4.h> | |
int main() { | |
CVC4::ExprManager _manager; | |
CVC4::SmtEngine _engine(& _manager); | |
_engine.setLogic("UFLIA"); | |
CVC4::Integer i = CVC4::Integer(1000); | |
_manager.mkConst(i); | |
return 0; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
CC=g++ | |
CFLAGS=-I /opt/cvc4-devel/include | |
LFLAGS=-L /opt/cvc4-devel/lib | |
LIBS=-lcvc4 -lgmp | |
all : inter | |
inter : inter.o | |
$(CC) $(LFLAGS) -o inter inter.o $(LIBS) | |
inter.o : inter.cc | |
$(CC) -c $(CFLAGS) inter.cc | |
clean : | |
rm inter | |
rm *.o | |
CVC4::Rational covers both integers and rationals, the proper call would be mkConst(CVC4::Rational(1000))
.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Compilation is accepted, but linking is not:
I believe this is due to the declaration of a generic mkConst in expr_manager.h :
even though the template is not instantiated for the Integer class. The actual
libcvc4.so
only contains the instantiated templates which would explain that the error only occurs at the linking stage.