projects
/
satune.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
e9ca288
)
bug fixes
author
Hamed Gorjiara
<hgorjiar@uci.edu>
Sat, 23 Feb 2019 08:22:32 +0000
(
00:22
-0800)
committer
Hamed Gorjiara
<hgorjiar@uci.edu>
Sat, 23 Feb 2019 08:22:32 +0000
(
00:22
-0800)
src/Interpreter/alloyinterpreter.cc
patch
|
blob
|
history
src/Interpreter/mathsatinterpreter.cc
patch
|
blob
|
history
src/Interpreter/smtinterpreter.cc
patch
|
blob
|
history
src/Interpreter/smtratinterpreter.cc
patch
|
blob
|
history
src/ccsolver.cc
patch
|
blob
|
history
src/ccsolver.h
patch
|
blob
|
history
diff --git
a/src/Interpreter/alloyinterpreter.cc
b/src/Interpreter/alloyinterpreter.cc
index c0e4a6094d97b8784fb8680eba9656f3e454d088..021b0878ed339fd6ee1b509095c24b101d57462b 100644
(file)
--- a/
src/Interpreter/alloyinterpreter.cc
+++ b/
src/Interpreter/alloyinterpreter.cc
@@
-101,6
+101,7
@@
void AlloyInterpreter::dumpHeader(){
}
void AlloyInterpreter::compileRunCommand(char * command, size_t size){
}
void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+ model_print("Calling Alloy...\n");
snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
}
snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
}
diff --git
a/src/Interpreter/mathsatinterpreter.cc
b/src/Interpreter/mathsatinterpreter.cc
index ce951533e36af5d9b703c8e65d47f4c923430829..5123efef72ba932e8a0bad8d836cfe540603a6b8 100644
(file)
--- a/
src/Interpreter/mathsatinterpreter.cc
+++ b/
src/Interpreter/mathsatinterpreter.cc
@@
-20,7
+20,8
@@
MathSATInterpreter::MathSATInterpreter(CSolver *solver):
}
void MathSATInterpreter::compileRunCommand(char * command , size_t size){
}
void MathSATInterpreter::compileRunCommand(char * command , size_t size){
- snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+ model_print("Calling MathSAT...\n");
+ snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
MathSATInterpreter::~MathSATInterpreter(){
}
MathSATInterpreter::~MathSATInterpreter(){
@@
-38,7
+39,7
@@
int MathSATInterpreter::getResult(){
strcpy ( cline, line.c_str() );
char valuestr [512];
uint id;
strcpy ( cline, line.c_str() );
char valuestr [512];
uint id;
- if (2 == sscanf(cline,"%*[^0123456789]%u
%*[^0123456789]
%s", &id, valuestr)){
+ if (2 == sscanf(cline,"%*[^0123456789]%u
%s", &id, valuestr)){
uint value;
if (strcmp (valuestr, "true)") == 0 ){
value =1;
uint value;
if (strcmp (valuestr, "true)") == 0 ){
value =1;
diff --git
a/src/Interpreter/smtinterpreter.cc
b/src/Interpreter/smtinterpreter.cc
index 82c887b244afa77156e97461382af4c395dc3a06..778093155da4386b04520a0382ddb054788d3f0f 100644
(file)
--- a/
src/Interpreter/smtinterpreter.cc
+++ b/
src/Interpreter/smtinterpreter.cc
@@
-101,7
+101,8
@@
void SMTInterpreter::dumpHeader(){
}
void SMTInterpreter::compileRunCommand(char * command, size_t size){
}
void SMTInterpreter::compileRunCommand(char * command, size_t size){
- snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+ model_print("Calling Z3...\n");
+ snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
string SMTInterpreter::negateConstraint(string constr){
}
string SMTInterpreter::negateConstraint(string constr){
diff --git
a/src/Interpreter/smtratinterpreter.cc
b/src/Interpreter/smtratinterpreter.cc
index ebe51135e3039f0d8e0fd14a89c03f5177172892..9742bda9669dfc26a4075c2386ab76def426b5e5 100644
(file)
--- a/
src/Interpreter/smtratinterpreter.cc
+++ b/
src/Interpreter/smtratinterpreter.cc
@@
-19,7
+19,8
@@
SMTRatInterpreter::SMTRatInterpreter(CSolver *solver):
}
void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
}
void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
- snprintf(command, size, "timeout %u ./smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+ model_print("Calling SMTRat...\n");
+ snprintf(command, size, "./run.sh timeout %u smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
SMTRatInterpreter::~SMTRatInterpreter(){
}
SMTRatInterpreter::~SMTRatInterpreter(){
diff --git
a/src/ccsolver.cc
b/src/ccsolver.cc
index 7acd00f4f4eb00ac48c9163e36527d6ea03b078b..8eb786dfb74013119be684c174e32f91a0d9931e 100644
(file)
--- a/
src/ccsolver.cc
+++ b/
src/ccsolver.cc
@@
-135,7
+135,6
@@
void printConstraints(void *solver) {
}
}
-
void serialize(void *solver) {
CCSOLVER(solver)->serialize();
}
void serialize(void *solver) {
CCSOLVER(solver)->serialize();
}
@@
-151,4
+150,4
@@
void setInterpreter(void *solver, unsigned int type){
void *clone(void *solver) {
return CCSOLVER(solver)->clone();
void *clone(void *solver) {
return CCSOLVER(solver)->clone();
-}
\ No newline at end of file
+}
diff --git
a/src/ccsolver.h
b/src/ccsolver.h
index 2051cc91b9126e2e8b8ccfbdd61c6cb9eca46df0..b10fa71681fc2bad67fd63fe6c6fce9e146b1398 100644
(file)
--- a/
src/ccsolver.h
+++ b/
src/ccsolver.h
@@
-41,7
+41,7
@@
int getOrderConstraintValue(void *solver,void *order, long first, long second);
void printConstraints(void *solver);
void serialize(void *solver);
void mustHaveValue(void *solver, void *element);
void printConstraints(void *solver);
void serialize(void *solver);
void mustHaveValue(void *solver, void *element);
-void set
AlloyEncoder(void *solver
);
+void set
Interpreter(void *solver, unsigned int type
);
void *clone(void *solver);
#ifdef __cplusplus
}
void *clone(void *solver);
#ifdef __cplusplus
}