From da3b2212ed6befc0d29646ef65570919377913fe Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 1 Oct 2018 11:07:13 -0700 Subject: Fix dumping pre/post preprocessing passes (#2469) This commit changes the hard-coded list of checks for preprocessing-related dump tags to take advantage of the new preprocessing pass registration mechanism from PR #2468. It also fixes a typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()` and adds a list of available passes to the `--dump help` output. --- src/preprocessing/preprocessing_pass.cpp | 3 ++- src/smt/dump.cpp | 38 ++++++++++++++------------------ src/smt/smt_engine.cpp | 4 ---- 3 files changed, 19 insertions(+), 26 deletions(-) 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/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); -- cgit v1.2.3 From d41c0aa8c7ec8d14ce07f5817da38895598e55da Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 1 Oct 2018 11:36:45 -0700 Subject: Fix compiler warnings. (#2555) --- src/prop/bvminisat/core/Solver.cc | 28 +++++++++++-------- src/prop/bvminisat/simp/SimpSolver.cc | 52 +++++++++++++++++++++-------------- src/prop/minisat/core/Solver.cc | 19 +++++++------ src/prop/minisat/simp/SimpSolver.cc | 52 +++++++++++++++++++++-------------- src/theory/arith/constraint.cpp | 5 ++-- 5 files changed, 93 insertions(+), 63 deletions(-) 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& 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& 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/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; -- cgit v1.2.3 From 6b718154dfbf5e9f8506d6911201bb7398ba8b48 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 1 Oct 2018 16:37:31 -0500 Subject: init scalar class members (coverity issues 1473720 and 1473721) (#2554) --- src/theory/quantifiers/sygus/enum_stream_substitution.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) { } -- cgit v1.2.3 From 968d12fb8dc668dde59b02923a6b9ec20ecbeb3f Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 1 Oct 2018 15:53:30 -0700 Subject: cmake: Add build target build-tests to build all test dependencies. (#2558) --- CMakeLists.txt | 4 +++- test/CMakeLists.txt | 6 +++++- test/java/CMakeLists.txt | 2 +- test/regress/CMakeLists.txt | 5 +---- test/system/CMakeLists.txt | 5 +---- test/unit/CMakeLists.txt | 5 +---- 6 files changed, 12 insertions(+), 15 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 4f17db83b..a42406dad 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -277,7 +277,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/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) -- cgit v1.2.3 From 64a0e3f1e4a5a8e3070eeadae0f6942b290c2974 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 1 Oct 2018 16:37:15 -0700 Subject: cmake: Generate compile_commands.json on configure. (#2559) --- CMakeLists.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index a42406dad..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) -- cgit v1.2.3