summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CMakeLists.txt8
-rw-r--r--src/preprocessing/preprocessing_pass.cpp3
-rw-r--r--src/prop/bvminisat/core/Solver.cc28
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc52
-rw-r--r--src/prop/minisat/core/Solver.cc19
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc52
-rw-r--r--src/smt/dump.cpp38
-rw-r--r--src/smt/smt_engine.cpp4
-rw-r--r--src/theory/arith/constraint.cpp5
-rw-r--r--src/theory/quantifiers/sygus/enum_stream_substitution.cpp4
-rw-r--r--test/CMakeLists.txt6
-rw-r--r--test/java/CMakeLists.txt2
-rw-r--r--test/regress/CMakeLists.txt5
-rw-r--r--test/system/CMakeLists.txt5
-rw-r--r--test/unit/CMakeLists.txt5
15 files changed, 130 insertions, 106 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4f17db83b..e850f9928 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -27,6 +27,10 @@ set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
set(CMAKE_C_STANDARD 99)
set(CMAKE_CXX_STANDARD 11)
+# Generate compile_commands.json, which can be used for various code completion
+# plugins.
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
#-----------------------------------------------------------------------------#
include(Helpers)
@@ -277,7 +281,9 @@ if(ENABLE_COVERAGE)
NAME coverage
EXECUTABLE
ctest -j${CTEST_NTHREADS} -LE "example"
- --output-on-failure $(ARGS) || exit 0)
+ --output-on-failure $(ARGS) || exit 0
+ DEPENDS
+ build-tests)
endif()
if(ENABLE_DEBUG_CONTEXT_MM)
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 6a1d89d33..120c68a91 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -36,7 +36,8 @@ PreprocessingPassResult PreprocessingPass::apply(
void PreprocessingPass::dumpAssertions(const char* key,
const AssertionPipeline& assertionList) {
- if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions::") + key)) {
+ if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
+ {
// Push the simplified assertions to the dump output stream
for (const auto& n : assertionList) {
Dump("assertions") << AssertCommand(Expr(n.toExpr()));
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 372f8eb04..a4b0248e0 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -357,8 +357,11 @@ void Solver::cancelUntil(int level) {
Var x = var(trail[c]);
assigns [x] = l_Undef;
if (marker[x] == 2) marker[x] = 1;
- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
- polarity[x] = sign(trail[c]);
+ if (phase_saving > 1
+ || ((phase_saving == 1) && c > trail_lim.last()))
+ {
+ polarity[x] = sign(trail[c]);
+ }
insertVarOrder(x); }
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
@@ -1080,16 +1083,19 @@ lbool Solver::search(int nof_conflicts, UIP uip)
cancelUntil(assumptions.size());
throw e;
}
-
- if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts ||
- !isWithinBudget) {
- // Reached bound on number of conflicts:
- Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
- progress_estimate = progressEstimate();
- cancelUntil(assumptions.size());
- return l_Undef;
+
+ if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
+ && conflictC >= nof_conflicts)
+ || !isWithinBudget)
+ {
+ // Reached bound on number of conflicts:
+ Debug("bvminisat::search")
+ << OUTPUT_TAG << " restarting " << std::endl;
+ progress_estimate = progressEstimate();
+ cancelUntil(assumptions.size());
+ return l_Undef;
}
-
+
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && !simplify()) {
Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 2fa8d472d..698d2a776 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -255,17 +255,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
- for (int i = 0; i < qs.size(); i++){
- if (var(qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(ps[j]) == var(qs[i]))
- if (ps[j] == ~qs[i])
- return false;
- else
- goto next;
- out_clause.push(qs[i]);
+ for (int i = 0; i < qs.size(); i++)
+ {
+ if (var(qs[i]) != v)
+ {
+ for (int j = 0; j < ps.size(); j++)
+ {
+ if (var(ps[j]) == var(qs[i]))
+ {
+ if (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ out_clause.push(qs[i]);
+ }
+ next:;
}
for (int i = 0; i < ps.size(); i++)
@@ -289,17 +295,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
size = ps.size()-1;
- for (int i = 0; i < qs.size(); i++){
- if (var(__qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(__ps[j]) == var(__qs[i]))
- if (__ps[j] == ~__qs[i])
- return false;
- else
- goto next;
- size++;
+ for (int i = 0; i < qs.size(); i++)
+ {
+ if (var(__qs[i]) != v)
+ {
+ for (int j = 0; j < ps.size(); j++)
+ {
+ if (var(__ps[j]) == var(__qs[i]))
+ {
+ if (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ size++;
+ }
+ next:;
}
return true;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index dbe417dbc..c8a2e16c2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1349,15 +1349,16 @@ lbool Solver::search(int nof_conflicts)
check_type = CHECK_WITH_THEORY;
}
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts ||
- !withinBudget(options::satConflictStep())) {
- // Reached bound on number of conflicts:
- progress_estimate = progressEstimate();
- cancelUntil(0);
- // [mdeters] notify theory engine of restarts for deferred
- // theory processing
- proxy->notifyRestart();
- return l_Undef;
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+ || !withinBudget(options::satConflictStep()))
+ {
+ // Reached bound on number of conflicts:
+ progress_estimate = progressEstimate();
+ cancelUntil(0);
+ // [mdeters] notify theory engine of restarts for deferred
+ // theory processing
+ proxy->notifyRestart();
+ return l_Undef;
}
// Simplify the set of problem clauses:
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 96fea2147..a101a0c2d 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -256,17 +256,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
- for (int i = 0; i < qs.size(); i++){
- if (var(qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(ps[j]) == var(qs[i]))
- if (ps[j] == ~qs[i])
- return false;
- else
- goto next;
- out_clause.push(qs[i]);
+ for (int i = 0; i < qs.size(); i++)
+ {
+ if (var(qs[i]) != v)
+ {
+ for (int j = 0; j < ps.size(); j++)
+ {
+ if (var(ps[j]) == var(qs[i]))
+ {
+ if (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ out_clause.push(qs[i]);
+ }
+ next:;
}
for (int i = 0; i < ps.size(); i++)
@@ -290,17 +296,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
size = ps.size()-1;
- for (int i = 0; i < qs.size(); i++){
- if (var(__qs[i]) != v){
- for (int j = 0; j < ps.size(); j++)
- if (var(__ps[j]) == var(__qs[i]))
- if (__ps[j] == ~__qs[i])
- return false;
- else
- goto next;
- size++;
+ for (int i = 0; i < qs.size(); i++)
+ {
+ if (var(__qs[i]) != v)
+ {
+ for (int j = 0; j < ps.size(); j++)
+ {
+ if (var(__ps[j]) == var(__qs[i]))
+ {
+ if (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ }
}
- next:;
+ size++;
+ }
+ next:;
}
return true;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 58a1e2912..eae11606f 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -15,8 +15,10 @@
**/
#include "smt/dump.h"
-#include "lib/strtok_r.h"
+
#include "base/output.h"
+#include "lib/strtok_r.h"
+#include "preprocessing/preprocessing_pass_registry.h"
namespace CVC4 {
@@ -55,25 +57,10 @@ void DumpC::setDumpFromString(const std::string& optarg) {
optargPtr + "'. Please consult --dump help.");
}
if(!strcmp(p, "everything")) {
- } else if(!strcmp(p, "definition-expansion")) {
- } else if(!strcmp(p, "boolean-terms")) {
- } else if(!strcmp(p, "constrain-subtypes")) {
- } else if(!strcmp(p, "substitution")) {
- } else if(!strcmp(p, "bv-to-bool")) {
- } else if(!strcmp(p, "bool-to-bv")) {
- } else if(!strcmp(p, "strings-pp")) {
- } else if(!strcmp(p, "skolem-quant")) {
- } else if(!strcmp(p, "simplify")) {
- } else if(!strcmp(p, "static-learning")) {
- } else if(!strcmp(p, "ite-removal")) {
- } else if(!strcmp(p, "repeat-simplify")) {
- } else if(!strcmp(p, "rewrite-apply-to-const")) {
- } else if(!strcmp(p, "theory-preprocessing")) {
- } else if(!strcmp(p, "nonclausal")) {
- } else if(!strcmp(p, "theorypp")) {
- } else if(!strcmp(p, "itesimp")) {
- } else if(!strcmp(p, "unconstrained")) {
- } else if(!strcmp(p, "repeatsimp")) {
+ }
+ else if (preprocessing::PreprocessingPassRegistry::getInstance().hasPass(
+ p))
+ {
} else {
throw OptionException(std::string("don't know how to dump `") +
optargPtr + "'. Please consult --dump help.");
@@ -116,6 +103,16 @@ void DumpC::setDumpFromString(const std::string& optarg) {
}
} else if(!strcmp(optargPtr, "help")) {
puts(s_dumpHelp.c_str());
+
+ std::stringstream ss;
+ ss << "Available preprocessing passes:\n";
+ for (const std::string& pass :
+ preprocessing::PreprocessingPassRegistry::getInstance()
+ .getAvailablePasses())
+ {
+ ss << "- " << pass << "\n";
+ }
+ puts(ss.str().c_str());
exit(1);
} else if(!strcmp(optargPtr, "bv-abstraction")) {
Dump.on("bv-abstraction");
@@ -140,7 +137,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
#endif /* CVC4_DUMPING */
}
-
const std::string DumpC::s_dumpHelp = "\
Dump modes currently supported by the --dump option:\n\
\n\
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b133f3a36..11c03de6c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2742,8 +2742,6 @@ static void dumpAssertions(const char* key,
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
{
- PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
-
spendResource(options::preprocessStep());
Assert(d_smt.d_pendingPops == 0);
try {
@@ -2972,8 +2970,6 @@ void SmtEnginePrivate::processAssertions() {
SubstitutionMap& top_level_substs =
d_preprocessingPassContext->getTopLevelSubstitutions();
- PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
-
// Dump the assertions
dumpAssertions("pre-everything", d_assertions);
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f5c3eac08..ff71f6432 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -711,9 +711,8 @@ bool Constraint::wellFormedFarkasProof() const {
}
Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
// 0 = lhs <= rhs < 0
- return
- (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) &&
- rhs.sgn() < 0;
+ return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
+ && rhs.sgn() < 0;
#else /* IS_PROOFS_BUILD */
return true;
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 3a879640f..b307876ed 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -29,7 +29,7 @@ namespace theory {
namespace quantifiers {
EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
- : d_tds(tds)
+ : d_tds(tds), d_first(true), d_curr_ind(0)
{
}
@@ -323,7 +323,7 @@ bool EnumStreamPermutation::PermutationState::getNextPermutation()
}
EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
- : d_tds(tds), d_stream_permutations(tds)
+ : d_tds(tds), d_stream_permutations(tds), d_curr_ind(0)
{
}
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index a79e96c65..f601e5247 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -4,6 +4,8 @@
# > regression tests of levels 0 and 1
# > system tests
+add_custom_target(build-tests)
+
# Note: Do not add custom targets for running tests (regress, systemtests,
# units) as dependencies to other run targets. This will result in executing
# tests multiple times. For example, if check would depend on regress it would
@@ -12,7 +14,9 @@
# Dependencies of check are added in the corresponding subdirectories.
add_custom_target(check
COMMAND
- ctest --output-on-failure -LE "regress[2-4]" -j${CTEST_NTHREADS} $(ARGS))
+ ctest --output-on-failure -LE "regress[2-4]" -j${CTEST_NTHREADS} $(ARGS)
+ DEPENDS
+ build-tests)
#-----------------------------------------------------------------------------#
# Add subdirectories
diff --git a/test/java/CMakeLists.txt b/test/java/CMakeLists.txt
index b6f0d035a..169013b84 100644
--- a/test/java/CMakeLists.txt
+++ b/test/java/CMakeLists.txt
@@ -18,7 +18,7 @@ add_jar(build-javatests
OUTPUT_NAME javatests
)
add_dependencies(build-javatests cvc4jar)
-add_dependencies(check build-javatests)
+add_dependencies(build-tests build-javatests)
# Add java tests to ctest
set(classpath "${CMAKE_CURRENT_BINARY_DIR}/javatests.jar")
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 79b706fdb..ecd98ddc2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2080,10 +2080,7 @@ get_target_property(path_to_cvc4 cvc4-bin RUNTIME_OUTPUT_DIRECTORY)
set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_regression.py)
add_custom_target(build-regress DEPENDS cvc4-bin)
-add_dependencies(check build-regress)
-if(ENABLE_COVERAGE)
- add_dependencies(coverage build-regress)
-endif()
+add_dependencies(build-tests build-regress)
add_custom_target(regress
COMMAND
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 36e6c4a37..9d0d8424a 100644
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -8,10 +8,7 @@ include_directories(${CMAKE_BINARY_DIR}/src)
# > system tests
add_custom_target(build-systemtests)
-add_dependencies(check build-systemtests)
-if(ENABLE_COVERAGE)
- add_dependencies(coverage build-systemtests)
-endif()
+add_dependencies(build-tests build-systemtests)
add_custom_target(systemtests
COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $(ARGS)
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index d362870c1..aa9248e6c 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -14,10 +14,7 @@ include_directories(${CMAKE_BINARY_DIR}/src)
# > unit tests
add_custom_target(build-units)
-add_dependencies(check build-units)
-if(ENABLE_COVERAGE)
- add_dependencies(coverage build-units)
-endif()
+add_dependencies(build-tests build-units)
add_custom_target(units
COMMAND ctest --output-on-failure -L "unit" -j${CTEST_NTHREADS} $(ARGS)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback