summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/assertions.cpp27
-rw-r--r--src/smt/assertions.h13
-rw-r--r--src/smt/process_assertions.cpp2
-rw-r--r--src/smt/proof_post_processor.cpp34
-rw-r--r--src/smt/set_defaults.cpp37
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback