diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/assertions.cpp | 27 | ||||
-rw-r--r-- | src/smt/assertions.h | 13 | ||||
-rw-r--r-- | src/smt/process_assertions.cpp | 2 | ||||
-rw-r--r-- | src/smt/proof_post_processor.cpp | 34 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 37 |
5 files changed, 82 insertions, 31 deletions
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 77646c002..9c24dd690 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -40,6 +40,7 @@ Assertions::Assertions(Env& env, AbstractValues& absv) d_produceAssertions(false), d_assertionList(userContext()), d_assertionListDefs(userContext()), + d_globalDefineFunLemmasIndex(userContext(), 0), d_globalNegation(false), d_assertions() { @@ -49,6 +50,22 @@ Assertions::~Assertions() { } +void Assertions::refresh() +{ + if (d_globalDefineFunLemmas != nullptr) + { + // Global definitions are asserted now to ensure they always exist. This is + // done at the beginning of preprocessing, to ensure that definitions take + // priority over, e.g. solving during preprocessing. See issue #7479. + size_t numGlobalDefs = d_globalDefineFunLemmas->size(); + for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++) + { + addFormula((*d_globalDefineFunLemmas)[i], false, true, false); + } + d_globalDefineFunLemmasIndex = numGlobalDefs; + } +} + void Assertions::finishInit() { // [MGD 10/20/2011] keep around in incremental mode, due to a @@ -107,16 +124,6 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions, ensureBoolean(n); addFormula(n, true, false, false); } - if (d_globalDefineFunLemmas != nullptr) - { - // Global definitions are asserted at check-sat-time because we have to - // make sure that they are always present (they are essentially level - // zero assertions) - for (const Node& lemma : *d_globalDefineFunLemmas) - { - addFormula(lemma, false, true, false); - } - } } void Assertions::assertFormula(const Node& n) diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 15131be60..5cda366e6 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -21,6 +21,7 @@ #include <vector> #include "context/cdlist.h" +#include "context/cdo.h" #include "expr/node.h" #include "preprocessing/assertion_pipeline.h" #include "smt/env_obj.h" @@ -56,6 +57,16 @@ class Assertions : protected EnvObj * without a check-sat. */ void clearCurrent(); + /** refresh + * + * Ensures that all global declarations have been processed in the current + * context. This may trigger substitutions to be added to the top-level + * substitution and/or formulas added to the current set of assertions. + * + * If global declarations are true, this method must be called before + * processing assertions. + */ + void refresh(); /* * Initialize a call to check satisfiability. This adds assumptions to * the list of assumptions maintained by this class, and finalizes the @@ -163,6 +174,8 @@ class Assertions : protected EnvObj * assert this list of definitions in each check-sat call. */ std::unique_ptr<std::vector<Node>> d_globalDefineFunLemmas; + /** The index of the above list that we have processed */ + context::CDO<size_t> d_globalDefineFunLemmasIndex; /** * The list of assumptions from the previous call to checkSatisfiability. * Note that if the last call to checkSatisfiability was an entailment check, diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 67e83bcd1..473b53015 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -93,6 +93,8 @@ void ProcessAssertions::spendResource(Resource r) bool ProcessAssertions::apply(Assertions& as) { + // must first refresh the assertions, in the case global declarations is true + as.refresh(); AssertionPipeline& assertions = as.getAssertionPipeline(); Assert(d_preprocessingPassContext != nullptr); // Dump the assertions diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a519ca6b5..17ea2c09c 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -18,6 +18,7 @@ #include "expr/skolem_manager.h" #include "options/proof_options.h" #include "preprocessing/assertion_pipeline.h" +#include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "smt/solver_engine.h" #include "theory/arith/arith_utilities.h" @@ -164,6 +165,8 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( CDProof* cdp) { Trace("smt-proof-pp-debug2") << push; + Trace("smt-proof-pp-debug2") << "Clause lits: " << clauseLits << "\n"; + Trace("smt-proof-pp-debug2") << "Target lits: " << targetClauseLits << "\n\n"; NodeManager* nm = NodeManager::currentNM(); Node trueNode = nm->mkConst(true); // get crowding lits and the position of the last clause that includes @@ -683,6 +686,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // literals, which could themselves add crowding literals. if (chainConclusion == args[0]) { + Trace("smt-proof-pp-debug") << "..same conclusion, DONE.\n"; cdp->addStep( chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs); return chainConclusion; @@ -695,11 +699,29 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, chainConclusion.end()}; std::set<Node> chainConclusionLitsSet{chainConclusion.begin(), chainConclusion.end()}; - // is args[0] a singleton clause? If it's not an OR node, then yes. - // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet + Trace("smt-proof-pp-debug2") + << "..chainConclusionLits: " << chainConclusionLits << "\n"; + Trace("smt-proof-pp-debug2") + << "..chainConclusionLitsSet: " << chainConclusionLitsSet << "\n"; std::vector<Node> conclusionLits; - // whether conclusion is singleton - if (chainConclusionLitsSet.count(args[0])) + // is args[0] a singleton clause? Yes if it's not an OR node. One might also + // think that it is a singleton if args[0] occurs in chainConclusionLitsSet. + // However it's not possible to know this only looking at the sets. For + // example with + // + // args[0] : (or b c) + // chairConclusionLitsSet : {b, c, (or b c)} + // + // we have that if args[0] occurs in the set but as a crowding literal, then + // args[0] is *not* a singleton clause. But if b and c were crowding + // literals, then args[0] would be a singleton clause. Since our intention + // is to determine who are the crowding literals exactly based on whether + // args[0] is a singleton or not, we must determine in another way whether + // args[0] is a singleton. + // + // Thus we rely on the standard utility to determine if args[0] is singleton + // based on the premises and arguments of the resolution + if (expr::isSingletonClause(args[0], children, chainResArgs)) { conclusionLits.push_back(args[0]); } @@ -716,6 +738,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // chain. if (chainConclusionLitsSet != conclusionLitsSet) { + Trace("smt-proof-pp-debug") << "..need to eliminate crowding lits.\n"; chainConclusion = eliminateCrowdingLits( chainConclusionLits, conclusionLits, children, args, cdp); // update vector of lits. Note that the set is no longer used, so we don't @@ -739,6 +762,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } else { + Trace("smt-proof-pp-debug") << "..add chainRes step directly.\n"; cdp->addStep( chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs); } @@ -751,6 +775,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // factoring if (chainConclusionLits.size() != conclusionLits.size()) { + Trace("smt-proof-pp-debug") << "..add factoring step.\n"; // We build it rather than taking conclusionLits because the order may be // different std::vector<Node> factoredLits; @@ -777,6 +802,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // reordering if (n != args[0]) { + Trace("smt-proof-pp-debug") << "..add reordering step.\n"; cdp->addStep(args[0], PfRule::REORDERING, {n}, {args[0]}); } return args[0]; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 7c813cee0..19eab3617 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -197,7 +197,8 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const } else if (!isSygus(opts) && logic.isQuantified() && (logic.isPure(THEORY_FP) - || (logic.isPure(THEORY_ARITH) && !logic.isLinear()))) + || (logic.isPure(THEORY_ARITH) && !logic.isLinear())) + && !opts.base.incrementalSolving) { opts.quantifiers.sygusInst = true; } @@ -301,7 +302,11 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const // formulas at preprocess time. // // We don't want to set this option when we are in logics that contain ALL. - if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) + // + // We also must enable stringExp if reElimAgg is true, since this introduces + // bounded quantifiers during preprocessing. + if ((!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) + || opts.strings.regExpElimAgg) { // If the user explicitly set a logic that includes strings, but is not // the generic "ALL" logic, then enable stringsExp. @@ -989,6 +994,18 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, << std::endl; opts.quantifiers.sygusInference = false; } + if (opts.quantifiers.sygusInst) + { + if (opts.quantifiers.sygusInstWasSetByUser) + { + reason << "sygus inst"; + return true; + } + Notice() << "SolverEngine: turning off sygus inst to support " + "incremental solving" + << std::endl; + opts.quantifiers.sygusInst = false; + } if (opts.smt.solveIntAsBV > 0) { reason << "solveIntAsBV"; @@ -1340,20 +1357,6 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { opts.quantifiers.macrosQuant = false; } - // HOL is incompatible with fmfBound - if (opts.quantifiers.fmfBound) - { - if (opts.quantifiers.fmfBoundWasSetByUser - || opts.quantifiers.fmfBoundLazyWasSetByUser - || opts.quantifiers.fmfBoundIntWasSetByUser) - { - Notice() << "Disabling bound finite-model finding since it is " - "incompatible with HOL.\n"; - } - - opts.quantifiers.fmfBound = false; - Trace("smt") << "turning off fmf-bound, since HOL\n"; - } } if (opts.quantifiers.fmfFunWellDefinedRelevant) { @@ -1628,7 +1631,7 @@ void SetDefaults::setDefaultsSygus(Options& opts) const reqBasicSygus = true; } if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify - || opts.quantifiers.sygusQueryGen) + || opts.quantifiers.sygusQueryGen != options::SygusQueryGenMode::NONE) { // rewrite rule synthesis implies that sygus stream must be true opts.quantifiers.sygusStream = true; |