summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile19
-rw-r--r--src/parser/smt/smt.cpp42
-rw-r--r--src/parser/smt/smt.h1
-rw-r--r--test/regress/regress0/uflia/error0.smt22
4 files changed, 40 insertions, 24 deletions
diff --git a/Makefile b/Makefile
index fad2350c4..8a6d80607 100644
--- a/Makefile
+++ b/Makefile
@@ -44,13 +44,30 @@ examples: all
YEAR := $(shell date +%Y)
submission:
if [ ! -e configure ]; then ./autogen.sh; fi
- ./configure competition --disable-shared --enable-static-binary --with-cln
+ ./configure competition --disable-shared --enable-static-binary --with-cln --with-portfolio
$(MAKE)
strip builds/bin/cvc4
$(MAKE) regress1
+ strip builds/bin/pcvc4
+ $(MAKE) regress1 BINARY=pcvc4
+ # main track
mkdir -p cvc4-smtcomp-$(YEAR)
cp -p builds/bin/cvc4 cvc4-smtcomp-$(YEAR)/cvc4
( echo '#!/bin/sh'; \
echo 'exec ./cvc4 -L smt2 --no-interactive' ) > cvc4-smtcomp-$(YEAR)/run
chmod 755 cvc4-smtcomp-$(YEAR)/run
tar cf cvc4-smtcomp-$(YEAR).tar cvc4-smtcomp-$(YEAR)
+ # parallel track
+ mkdir -p cvc4-parallel-smtcomp-$(YEAR)
+ cp -p builds/bin/pcvc4 cvc4-parallel-smtcomp-$(YEAR)/pcvc4
+ ( echo '#!/bin/sh'; \
+ echo 'exec ./pcvc4 -L smt2 --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run
+ chmod 755 cvc4-parallel-smtcomp-$(YEAR)/run
+ tar cf cvc4-parallel-smtcomp-$(YEAR).tar cvc4-parallel-smtcomp-$(YEAR)
+ # application track
+ mkdir -p cvc4-application-smtcomp-$(YEAR)
+ cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/cvc4
+ ( echo '#!/bin/sh'; \
+ echo 'exec ./cvc4 -L smt2 --no-interactive --incremental' ) > cvc4-application-smtcomp-$(YEAR)/run
+ chmod 755 cvc4-application-smtcomp-$(YEAR)/run
+ tar cf cvc4-application-smtcomp-$(YEAR).tar cvc4-application-smtcomp-$(YEAR)
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 4d3c1d086..e554cee10 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -175,11 +175,6 @@ bool Smt::logicIsSet() {
return d_logicSet;
}
-inline void Smt::addUf() {
- addTheory(Smt::THEORY_EMPTY);
- addOperator(kind::APPLY_UF);
-}
-
void Smt::setLogic(const std::string& name) {
d_logicSet = true;
d_logic = toLogic(name);
@@ -209,24 +204,25 @@ void Smt::setLogic(const std::string& name) {
case QF_UFLIA:
case QF_UFNIA:// nonstandard logic
addTheory(THEORY_INTS);
- addUf();
+ addOperator(kind::APPLY_UF);
break;
case QF_UFLRA:
case QF_UFNRA:
addTheory(THEORY_REALS);
- addUf();
+ addOperator(kind::APPLY_UF);
break;
case QF_UFLIRA:// nonstandard logic
case QF_UFNIRA:// nonstandard logic
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
- addUf();
+ addOperator(kind::APPLY_UF);
break;
case QF_UF:
- addUf();
+ addTheory(THEORY_EMPTY);
+ addOperator(kind::APPLY_UF);
break;
case QF_BV:
@@ -239,25 +235,25 @@ void Smt::setLogic(const std::string& name) {
break;
case QF_UFBV:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_BITVECTORS);
break;
case QF_AUFBV:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
break;
case QF_AUFBVLIA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
addTheory(THEORY_INTS);
break;
case QF_AUFBVLRA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
addTheory(THEORY_REALS);
@@ -265,13 +261,13 @@ void Smt::setLogic(const std::string& name) {
case QF_AUFLIA:
addTheory(THEORY_INT_ARRAYS_EX);
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
break;
case QF_AUFLIRA:
addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
break;
@@ -281,14 +277,14 @@ void Smt::setLogic(const std::string& name) {
/* fall through */
case QF_ALL_SUPPORTED:
addTheory(THEORY_ARRAYS_EX);
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
addTheory(THEORY_BITVECTORS);
break;
case AUFLIA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_INT_ARRAYS_EX);
addTheory(THEORY_QUANTIFIERS);
@@ -296,7 +292,7 @@ void Smt::setLogic(const std::string& name) {
case AUFLIRA:
case AUFNIRA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
@@ -304,20 +300,24 @@ void Smt::setLogic(const std::string& name) {
break;
case LRA:
+ addTheory(THEORY_REALS);
+ addTheory(THEORY_QUANTIFIERS);
+ break;
+
case UFNIA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_QUANTIFIERS);
break;
case UFNIRA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
addTheory(THEORY_QUANTIFIERS);
break;
case UFLRA:
- addUf();
+ addOperator(kind::APPLY_UF);
addTheory(THEORY_REALS);
addTheory(THEORY_QUANTIFIERS);
break;
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 7b1dfc345..b82d3a01c 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -116,7 +116,6 @@ public:
private:
void addArithmeticOperators();
- void addUf();
static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
};/* class Smt */
diff --git a/test/regress/regress0/uflia/error0.smt2 b/test/regress/regress0/uflia/error0.smt2
index 614645cb4..73177a252 100644
--- a/test/regress/regress0/uflia/error0.smt2
+++ b/test/regress/regress0/uflia/error0.smt2
@@ -3,7 +3,7 @@
(declare-sort U 0)
(set-info :source "Currently this example asserts both a literal and its negation to a theory.")
(set-info :status unsat)
-(set-info :category industrial)
+(set-info :category "industrial")
(set-info :difficulty 0)
(declare-fun arg0 () Int)
(declare-fun arg1 () Int)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback