This eliminates the static member `s_uninterpretedSortOwner` from Theory which seems to be the cause of several issues related to the array solver in incremental mode, and with check-unsat-cores. This is moved to a data member of Env. This eliminates a static access to `theoryOfMode` from within theoryOf calls.
Note that static calls to `Theory::theoryOf` or `Theory::isLeafOf` now assume type-based theoryOf mode as a default argument. Thus, the preferred method for determining theoryOf types and terms is through `Env` now.
This fixes issues with the array solver in incremental mode.
The root issue is that spawning subsolvers (e.g. for check-unsat-core) can overwrite `s_uninterpretedSortOwner`. This means that a second call to `check-sat` (which does not reinitialize set_defaults) will use the *overwrtten* setting, which can be different from what was used for the first check-sat. In particular, for #5720, the uninterpreted sort owner changes from ARRAYS to UF at the 2nd call, and the array theory solver fails to send an extensionality lemma.
This commit also simplifies `Theory::theoryOf` slightly.
Fixes https://github.com/cvc5/cvc5-wishues/issues/52.
Fixes https://github.com/cvc5/cvc5/issues/5720.
Fixes https://github.com/cvc5/cvc5/issues/6276 .
Fixes https://github.com/cvc5/cvc5/issues/5836.
bool ITESimplifier::leavesAreConst(TNode e)
{
- return leavesAreConst(e, theory::Theory::theoryOf(e));
+ return leavesAreConst(e, d_env.theoryOf(e));
}
void ITESimplifier::clearSimpITECaches()
bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
{
Assert((e.getKind() == kind::ITE && !e.getType().isBoolean())
- || theory::Theory::theoryOf(e) != theory::THEORY_BOOL);
+ || d_env.theoryOf(e) != theory::THEORY_BOOL);
if (e.isConst())
{
return true;
// If node has no ITE's or already in the cache we're done, pop from the
// stack
if (current.getNumChildren() == 0
- || (theory::Theory::theoryOf(current) != theory::THEORY_BOOL
+ || (d_env.theoryOf(current) != theory::THEORY_BOOL
&& !containsTermITE(current)))
{
d_simpITECache[current] = current;
Node result = builder;
// If this is an atom, we process it
- if (theory::Theory::theoryOf(result) != theory::THEORY_BOOL
+ if (d_env.theoryOf(result) != theory::THEORY_BOOL
&& result.getType().isBoolean())
{
result = simpITEAtom(result);
namespace cvc5 {
namespace prop {
-CnfStream::CnfStream(SatSolver* satSolver,
+CnfStream::CnfStream(Env& env,
+ SatSolver* satSolver,
Registrar* registrar,
- context::Context* context,
- Env* env,
- ResourceManager* rm,
+ context::Context* c,
FormulaLitPolicy flpol,
std::string name)
- : d_satSolver(satSolver),
- d_env(env),
- d_booleanVariables(context),
- d_notifyFormulas(context),
- d_nodeToLiteralMap(context),
- d_literalToNodeMap(context),
+ : EnvObj(env),
+ d_satSolver(satSolver),
+ d_booleanVariables(c),
+ d_notifyFormulas(c),
+ d_nodeToLiteralMap(c),
+ d_literalToNodeMap(c),
d_flitPolicy(flpol),
d_registrar(registrar),
d_name(name),
d_removable(false),
- d_resourceManager(rm),
d_stats(name)
{
}
}
// remove top level negation
n = n.getKind() == kind::NOT ? n[0] : n;
- if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+ if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
{
// If we were called with something other than a theory atom (or
// Boolean variable), we get a SatLiteral that is definitionally
Trace("cnf") << "convertAndAssert(" << node
<< ", negated = " << (negated ? "true" : "false") << ")\n";
- d_resourceManager->spendResource(Resource::CnfStep);
+ resourceManager()->spendResource(Resource::CnfStep);
switch(node.getKind()) {
case kind::AND: convertAndAssertAnd(node, negated); break;
#include "prop/proof_cnf_stream.h"
#include "prop/registrar.h"
#include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
namespace cvc5 {
* each subexpression in the constructed equi-satisfiable formula, then
* substitute the new literal for the formula, and so on, recursively.
*/
-class CnfStream {
+class CnfStream : protected EnvObj
+{
friend PropEngine;
friend ProofCnfStream;
* and sends the generated clauses and to the given SAT solver. This does not
* take ownership of satSolver, registrar, or context.
*
+ * @param env reference to the environment
* @param satSolver the sat solver to use.
* @param registrar the entity that takes care of preregistration of Nodes.
- * @param context the context that the CNF should respect.
- * @param env Reference to the environment of the smt engine. Assertions
- * will not be dumped if env == nullptr.
- * @param rm the resource manager of the CNF stream
+ * @param c the context that the CNF should respect.
* @param flpol policy for literals corresponding to formulas (those that are
* not-theory literals).
* @param name string identifier to distinguish between different instances
* even for non-theory literals.
*/
- CnfStream(SatSolver* satSolver,
+ CnfStream(Env& env,
+ SatSolver* satSolver,
Registrar* registrar,
- context::Context* context,
- Env* env,
- ResourceManager* rm,
+ context::Context* c,
FormulaLitPolicy flpol = FormulaLitPolicy::INTERNAL,
std::string name = "");
/**
/** The SAT solver we will be using */
SatSolver* d_satSolver;
- /** Pointer to the env of the smt engine */
- Env* d_env;
-
/** Boolean variables that we translated */
context::CDList<TNode> d_booleanVariables;
namespace cvc5 {
namespace prop {
-ProofCnfStream::ProofCnfStream(context::UserContext* u,
+ProofCnfStream::ProofCnfStream(Env& env,
CnfStream& cnfStream,
- SatProofManager* satPM,
- ProofNodeManager* pnm)
- : d_cnfStream(cnfStream),
+ SatProofManager* satPM)
+ : EnvObj(env),
+ d_cnfStream(cnfStream),
d_satPM(satPM),
- d_proof(pnm, nullptr, u, "ProofCnfStream::LazyCDProof"),
- d_blocked(u)
+ d_proof(env.getProofNodeManager(),
+ nullptr,
+ userContext(),
+ "ProofCnfStream::LazyCDProof"),
+ d_blocked(userContext())
{
}
// remove top level negation. We don't need to track this because it's a
// literal.
n = n.getKind() == kind::NOT ? n[0] : n;
- if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+ if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
{
// These are not removable
d_cnfStream.d_removable = false;
#include "proof/theory_proof_step_buffer.h"
#include "prop/cnf_stream.h"
#include "prop/sat_proof_manager.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace prop {
* that getting the proof of a clausified formula will also extend to its
* registered proof generator.
*/
-class ProofCnfStream : public ProofGenerator
+class ProofCnfStream : protected EnvObj, public ProofGenerator
{
public:
- ProofCnfStream(context::UserContext* u,
- CnfStream& cnfStream,
- SatProofManager* satPM,
- ProofNodeManager* pnm);
+ ProofCnfStream(Env& env, CnfStream& cnfStream, SatProofManager* satPM);
/** Invokes getProofFor of the underlying LazyCDProof */
std::shared_ptr<ProofNode> getProofFor(Node f) override;
CnfStream& d_cnfStream;
/** The proof manager of underlying SAT solver associated with this stream. */
SatProofManager* d_satPM;
- /** The proof node manager. */
- ProofNodeManager* d_pnm;
/** The user-context-dependent proof object. */
LazyCDProof d_proof;
/** An accumulator of steps that may be applied to normalize the clauses
Debug("prop") << "Constructing the PropEngine" << std::endl;
context::UserContext* userContext = d_env.getUserContext();
ProofNodeManager* pnm = d_env.getProofNodeManager();
- ResourceManager* rm = d_env.getResourceManager();
options::DecisionMode dmode = options().decision.decisionMode;
if (dmode == options::DecisionMode::JUSTIFICATION
// theory proxy first
d_theoryProxy = new TheoryProxy(
d_env, this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get());
- d_cnfStream = new CnfStream(d_satSolver,
+ d_cnfStream = new CnfStream(env,
+ d_satSolver,
d_theoryProxy,
userContext,
- &d_env,
- rm,
FormulaLitPolicy::TRACK,
"prop");
if (satProofs)
{
d_pfCnfStream.reset(new ProofCnfStream(
- userContext,
+ env,
*d_cnfStream,
- static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager(),
- pnm));
+ static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager()));
d_ppm.reset(
new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
}
}
if( result == SAT_VALUE_UNKNOWN ) {
- ResourceManager* rm = d_env.getResourceManager();
+ ResourceManager* rm = resourceManager();
Result::UnknownExplanation why = Result::INTERRUPTED;
if (rm->outOfTime())
{
#include "smt/solver_engine_stats.h"
#include "theory/evaluator.h"
#include "theory/rewriter.h"
+#include "theory/theory.h"
#include "theory/trust_substitutions.h"
#include "util/resource_manager.h"
#include "util/statistics_registry.h"
d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)),
d_options(),
d_originalOptions(opts),
- d_resourceManager()
+ d_resourceManager(),
+ d_uninterpretedSortOwner(theory::THEORY_UF)
{
if (opts != nullptr)
{
d_options.quantifiers.finiteModelFind);
}
+void Env::setUninterpretedSortOwner(theory::TheoryId theory)
+{
+ d_uninterpretedSortOwner = theory;
+}
+
+theory::TheoryId Env::getUninterpretedSortOwner() const
+{
+ return d_uninterpretedSortOwner;
+}
+
+theory::TheoryId Env::theoryOf(TypeNode typeNode) const
+{
+ return theory::Theory::theoryOf(typeNode, d_uninterpretedSortOwner);
+}
+
+theory::TheoryId Env::theoryOf(TNode node) const
+{
+ return theory::Theory::theoryOf(
+ node, d_options.theory.theoryOfMode, d_uninterpretedSortOwner);
+}
+
} // namespace cvc5
#include "options/options.h"
#include "proof/method_id.h"
#include "theory/logic_info.h"
+#include "theory/theory_id.h"
#include "util/statistics_registry.h"
namespace cvc5 {
*/
bool isFiniteType(TypeNode tn) const;
+ /**
+ * Set the owner of the uninterpreted sort.
+ */
+ void setUninterpretedSortOwner(theory::TheoryId theory);
+
+ /**
+ * Get the owner of the uninterpreted sort.
+ */
+ theory::TheoryId getUninterpretedSortOwner() const;
+
+ /**
+ * Return the ID of the theory responsible for the given type.
+ */
+ theory::TheoryId theoryOf(TypeNode typeNode) const;
+
+ /**
+ * Returns the ID of the theory responsible for the given node.
+ */
+ theory::TheoryId theoryOf(TNode node) const;
+
private:
/* Private initialization ------------------------------------------------- */
const Options* d_originalOptions;
/** Manager for limiting time and abstract resource usage. */
std::unique_ptr<ResourceManager> d_resourceManager;
+ /** The theory that owns the uninterpreted sort. */
+ theory::TheoryId d_uninterpretedSortOwner;
}; /* class Env */
} // namespace cvc5
result.push(ret.isNull() ? n : ret);
continue;
}
- theory::TheoryId tid = theory::Theory::theoryOf(node);
+ theory::TheoryId tid = d_env.theoryOf(node);
theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);
Assert(tr != NULL);
{
// get the kind of rewrite
MethodId idr = MethodId::RW_REWRITE;
- TheoryId theoryId = Theory::theoryOf(args[0]);
+ TheoryId theoryId = d_env.theoryOf(args[0]);
if (args.size() >= 2)
{
getMethodId(args[1], idr);
&& (!logic.isQuantified()
|| (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
{
- Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
+ d_env.setUninterpretedSortOwner(THEORY_ARRAYS);
}
else
{
- Theory::setUninterpretedSortOwner(THEORY_UF);
+ d_env.setUninterpretedSortOwner(THEORY_UF);
}
if (!opts.smt.simplifyWithCareEnabledWasSetByUser)
// Also preprocess it before we send it out. This is important since
// arithmetic may prefer eliminating equalities.
TrustNode teq;
- if (Theory::theoryOf(eq) == THEORY_ARITH)
+ if (d_env.theoryOf(eq) == THEORY_ARITH)
{
teq = d_ppre.ppRewriteEq(eq);
eq = teq.isNull() ? eq : teq.getNode();
{
return d_ppre.ppRewriteEq(atom);
}
- Assert(Theory::theoryOf(atom) == THEORY_ARITH);
+ Assert(d_env.theoryOf(atom) == THEORY_ARITH);
// Eliminate operators. Notice we must do this here since other
// theories may generate lemmas that involve non-standard operators. For
// example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
d_env.getResourceManager(),
"theory::bv::BVSolverBitblast::"));
}
- d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+ d_cnfStream.reset(new prop::CnfStream(d_env,
+ d_satSolver.get(),
d_bbRegistrar.get(),
d_nullContext.get(),
- nullptr,
- d_env.getResourceManager(),
prop::FormulaLitPolicy::INTERNAL,
"theory::bv::BVSolverBitblast"));
}
continue;
}
- if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
+ if (theory::Theory::theoryOf(n, options::TheoryOfMode::THEORY_OF_TERM_BASED)
== theory::THEORY_BV)
{
Kind k = n.getKind();
default:
{
- Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
+ Trace("evaluator") << "Evaluation of " << currNode[0].getKind()
<< " not supported" << std::endl;
results[currNode] = EvalResult();
evalAsNode[currNode] =
if (visited.find(tn) == visited.end())
{
visited[tn] = true;
- TheoryId tid = Theory::theoryOf(tn);
+ TheoryId tid = d_env.theoryOf(tn);
registerTheoryId(tid);
if (tn.isDatatype())
{
std::unordered_set<Node> lits;
for (unsigned r = 0; r < 2; r++)
{
- TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
+ TheoryId tid = r == 0 ? d_env.theoryOf(pvtn) : THEORY_UF;
Trace("cegqi-inst-debug2") << " look at assertions of " << tid << std::endl;
std::map<TheoryId, std::vector<Node> >::iterator ita =
d_curr_asserts.find(tid);
while( !eqcs_i.isFinished() ){
Node r = *eqcs_i;
TypeNode rtn = r.getType();
- TheoryId tid = Theory::theoryOf( rtn );
+ TheoryId tid = d_env.theoryOf(rtn);
//if we care about the theory of this eqc
if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){
if (rtn.isRealOrInt())
TNode current,
TNode parent)
{
- TheoryId currentTheoryId = Theory::theoryOf(current);
+ TheoryId currentTheoryId = env.theoryOf(current);
if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
{
// current theory not visited, return false
// The current theory has already visited it, so now it depends on the parent
// and the type
- TheoryId parentTheoryId = Theory::theoryOf(parent);
+ TheoryId parentTheoryId = env.theoryOf(parent);
if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
{
// parent theory not visited, return false
// current and parent are the same theory, and we are infinite, return true
return true;
}
- TheoryId typeTheoryId = Theory::theoryOf(type);
+ TheoryId typeTheoryId = env.theoryOf(type);
return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
}
TheoryIdSet preregTheories)
{
// Preregister with the current theory, if necessary
- TheoryId currentTheoryId = Theory::theoryOf(current);
+ TheoryId currentTheoryId = env.theoryOf(current);
preRegisterWithTheory(
te, visitedTheories, currentTheoryId, current, parent, preregTheories);
if (current != parent)
{
// preregister with parent theory, if necessary
- TheoryId parentTheoryId = Theory::theoryOf(parent);
+ TheoryId parentTheoryId = env.theoryOf(parent);
preRegisterWithTheory(
te, visitedTheories, parentTheoryId, current, parent, preregTheories);
if (currentTheoryId != parentTheoryId || env.isFiniteType(type))
{
// preregister with the type's theory, if necessary
- TheoryId typeTheoryId = Theory::theoryOf(type);
+ TheoryId typeTheoryId = env.theoryOf(type);
preRegisterWithTheory(
te, visitedTheories, typeTheoryId, current, parent, preregTheories);
}
TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
// If there is more than two theories and a new one has been added notify the shared terms database
- TheoryId currentTheoryId = Theory::theoryOf(current);
+ TheoryId currentTheoryId = d_env.theoryOf(current);
if (TheoryIdSetUtil::setDifference(
visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
{
namespace cvc5 {
namespace theory {
-/** Default value for the uninterpreted sorts is the UF theory */
-TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
-
std::ostream& operator<<(std::ostream& os, Theory::Effort level){
switch(level){
case Theory::EFFORT_STANDARD:
finishInit();
}
-TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
+TheoryId Theory::theoryOf(TNode node,
+ options::TheoryOfMode mode,
+ TheoryId usortOwner)
{
TheoryId tid = THEORY_BUILTIN;
switch(mode) {
}
else
{
- tid = Theory::theoryOf(node.getType());
+ tid = theoryOf(node.getType(), usortOwner);
}
}
else if (node.getKind() == kind::EQUAL)
{
// Equality is owned by the theory that owns the domain
- tid = Theory::theoryOf(node[0].getType());
+ tid = theoryOf(node[0].getType(), usortOwner);
}
else
{
// Variables
if (node.isVar())
{
- if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
+ if (theoryOf(node.getType(), usortOwner) != theory::THEORY_BOOL)
{
// We treat the variables as uninterpreted
- tid = s_uninterpretedSortOwner;
+ tid = THEORY_UF;
}
else
{
}
else if (node.getKind() == kind::EQUAL)
{ // Equality
- // If one of them is an ITE, it's irelevant, since they will get
- // replaced out anyhow
- if (node[0].getKind() == kind::ITE)
- {
- tid = Theory::theoryOf(node[0].getType());
- }
- else if (node[1].getKind() == kind::ITE)
+ TNode l = node[0];
+ TNode r = node[1];
+ TypeNode ltype = l.getType();
+ TypeNode rtype = r.getType();
+ // If the types are different, we must assign based on type due
+ // to handling subtypes (limited to arithmetic). Also, if we are
+ // a Boolean equality, we must assign THEORY_BOOL.
+ if (ltype != rtype || ltype.isBoolean())
{
- tid = Theory::theoryOf(node[1].getType());
+ tid = theoryOf(ltype, usortOwner);
}
else
{
- TNode l = node[0];
- TNode r = node[1];
- TypeNode ltype = l.getType();
- TypeNode rtype = r.getType();
- // If the types are different, we must assign based on type due
- // to handling subtypes (limited to arithmetic). Also, if we are
- // a Boolean equality, we must assign THEORY_BOOL.
- if (ltype != rtype || ltype.isBoolean())
+ // If both sides belong to the same theory the choice is easy
+ TheoryId T1 = theoryOf(l, mode, usortOwner);
+ TheoryId T2 = theoryOf(r, mode, usortOwner);
+ if (T1 == T2)
{
- tid = Theory::theoryOf(ltype);
+ tid = T1;
}
else
{
- // If both sides belong to the same theory the choice is easy
- TheoryId T1 = Theory::theoryOf(l);
- TheoryId T2 = Theory::theoryOf(r);
- if (T1 == T2)
+ TheoryId T3 = theoryOf(ltype, usortOwner);
+ // This is a case of
+ // * x*y = f(z) -> UF
+ // * x = c -> UF
+ // * f(x) = read(a, y) -> either UF or ARRAY
+ // at least one of the theories has to be parametric, i.e. theory
+ // of the type is different from the theory of the term
+ if (T1 == T3)
+ {
+ tid = T2;
+ }
+ else if (T2 == T3)
{
tid = T1;
}
else
{
- TheoryId T3 = Theory::theoryOf(ltype);
- // This is a case of
- // * x*y = f(z) -> UF
- // * x = c -> UF
- // * f(x) = read(a, y) -> either UF or ARRAY
- // at least one of the theories has to be parametric, i.e. theory
- // of the type is different from the theory of the term
- if (T1 == T3)
- {
- tid = T2;
- }
- else if (T2 == T3)
- {
- tid = T1;
- }
- else
- {
- // If both are parametric, we take the smaller one (arbitrary)
- tid = T1 < T2 ? T1 : T2;
- }
+ // If both are parametric, we take the smaller one (arbitrary)
+ tid = T1 < T2 ? T1 : T2;
}
}
}
default:
Unreachable();
}
- Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
return tid;
}
termSet.insert(cur);
}
// traverse owned terms, don't go under quantifiers
- if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id)
+ if ((k == kind::NOT || k == kind::EQUAL || d_env.theoryOf(cur) == d_id)
&& !cur.isClosure())
{
visit.insert(visit.end(), cur.begin(), cur.end());
*/
virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
- /**
- * The theory that owns the uninterpreted sort.
- */
- static TheoryId s_uninterpretedSortOwner;
-
void printFacts(std::ostream& os) const;
void debugPrintFacts() const;
/**
* Return the ID of the theory responsible for the given type.
*/
- static inline TheoryId theoryOf(TypeNode typeNode)
+ static inline TheoryId theoryOf(TypeNode typeNode,
+ TheoryId usortOwner = theory::THEORY_UF)
{
- Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
TheoryId id;
if (typeNode.getKind() == kind::TYPE_CONSTANT)
{
}
if (id == THEORY_BUILTIN)
{
- Trace("theory::internal")
- << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner
- << std::endl;
- return s_uninterpretedSortOwner;
+ return usortOwner;
}
return id;
}
/**
* Returns the ID of the theory responsible for the given node.
*/
- static TheoryId theoryOf(options::TheoryOfMode mode, TNode node);
-
- /**
- * Returns the ID of the theory responsible for the given node.
- */
- static inline TheoryId theoryOf(TNode node)
- {
- return theoryOf(options::theoryOfMode(), node);
- }
-
- /**
- * Set the owner of the uninterpreted sort.
- */
- static void setUninterpretedSortOwner(TheoryId theory)
- {
- s_uninterpretedSortOwner = theory;
- }
-
- /**
- * Get the owner of the uninterpreted sort.
- */
- static TheoryId getUninterpretedSortOwner()
- {
- return s_uninterpretedSortOwner;
- }
+ static TheoryId theoryOf(
+ TNode node,
+ options::TheoryOfMode mode = options::TheoryOfMode::THEORY_OF_TYPE_BASED,
+ TheoryId usortOwner = theory::THEORY_UF);
/**
- * Checks if the node is a leaf node of this theory
+ * Checks if the node is a leaf node of this theory.
*/
inline bool isLeaf(TNode node) const
{
- return node.getNumChildren() == 0 || theoryOf(node) != d_id;
+ return node.getNumChildren() == 0
+ || theoryOf(node, options().theory.theoryOfMode) != d_id;
}
/**
* Checks if the node is a leaf node of a theory.
*/
- inline static bool isLeafOf(TNode node, TheoryId theoryId)
+ inline static bool isLeafOf(
+ TNode node,
+ TheoryId theoryId,
+ options::TheoryOfMode mode = options::TheoryOfMode::THEORY_OF_TYPE_BASED)
{
- return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
+ return node.getNumChildren() == 0 || theoryOf(node, mode) != theoryId;
}
/** Returns true if the assertFact queue is empty*/
TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
- if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
- Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
+ theory::TheoryId tid = d_env.theoryOf(atom);
+ if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
+ {
stringstream ss;
ss << "The logic was specified as " << d_logicInfo.getLogicString()
- << ", which doesn't include " << Theory::theoryOf(atom)
+ << ", which doesn't include " << tid
<< ", but got a preprocessing-time fact for that theory." << endl
<< "The fact:" << endl
<< literal;
assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
{
// Is it preregistered
- bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
+ bool preregistered = d_propEngine->isSatLiteral(assertion)
+ && d_env.theoryOf(assertion) == toTheoryId;
// We assert it
theoryOf(toTheoryId)->assertFact(assertion, preregistered);
// Mark that we have more information
assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
{
// Check if has been pre-registered with the theory
- bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
+ bool preregistered = d_propEngine->isSatLiteral(assertion)
+ && d_env.theoryOf(assertion) == toTheoryId;
// Assert away
theoryOf(toTheoryId)->assertFact(assertion, preregistered);
d_factsAsserted = true;
// to the assert the equality to the interested theories
if (atom.getKind() == kind::EQUAL) {
// Assert it to the the owning theory
- assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+ assertToTheory(literal,
+ literal,
+ /* to */ d_env.theoryOf(atom),
+ /* from */ THEORY_SAT_SOLVER);
// Shared terms manager will assert to interested theories directly, as
// the terms become shared
assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
} else {
// Not an equality, just assert to the appropriate theory
- assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+ assertToTheory(literal,
+ literal,
+ /* to */ d_env.theoryOf(atom),
+ /* from */ THEORY_SAT_SOLVER);
}
} else {
// Assert the fact to the appropriate theory directly
- assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+ assertToTheory(literal,
+ literal,
+ /* to */ d_env.theoryOf(atom),
+ /* from */ THEORY_SAT_SOLVER);
}
}
}
Assert(d_sharedSolver->isShared(var))
<< "node " << var << " is not shared" << std::endl;
- return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
+ return theoryOf(d_env.theoryOf(var.getType()))->getModelValue(var);
}
TrustNode TheoryEngine::getExplanation(TNode node)
// If the theory is asking about a different form, or the form is ok but if will go to a different theory
// then we must figure it out
- if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
+ if (eqNormalized != eq || d_env.theoryOf(eq) != atomsTo)
+ {
// If you get eqNormalized, send atoms[i] to atomsTo
d_atomRequests.add(eqNormalized, eq, atomsTo);
}
return std::pair<bool, Node>(false, Node::null());
}else{
//it is a theory atom
- theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
+ theory::TheoryId tid = Theory::theoryOf(atom, mode);
theory::Theory* th = theoryOf(tid);
Assert(th != NULL);
*/
theory::Theory* theoryOf(TNode node) const
{
- return d_theoryTable[theory::Theory::theoryOf(node)];
+ return d_theoryTable[d_env.theoryOf(node)];
}
/**
regress0/arrays/issue4780-3.smt2
regress0/arrays/issue4780.smt2
regress0/arrays/issue4927-unsat-cores.smt2
+ regress0/arrays/issue5720.smt2
+ regress0/arrays/issue5836-2.smt2
+ regress0/arrays/issue5836.smt2
+ regress0/arrays/issue6276-2.smt2
+ regress0/arrays/issue6276.smt2
regress0/arrays/issue6807-idem-rew.smt2
regress0/arrays/issue7596-define-array-uminus.smt2
regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
--- /dev/null
+; COMMAND-LINE: -i
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic QF_ALIA)
+(set-option :check-unsat-cores true)
+(set-option :fmf-fun true)
+(declare-fun arr0 () (Array Bool Int))
+(declare-fun arr1 () (Array Int (Array Bool Int)))
+(assert (xor true (= arr1 (store arr1 0 arr0))))
+(push)
+(assert false)
+(check-sat)
+(pop)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_UFNRA)
+(set-info :status sat)
+(declare-fun ufrr5 (Real Real Real Real Real) Real)
+(declare-fun r5 () Real)
+(declare-fun r6 () Real)
+(declare-fun r37 () Real)
+(declare-fun r58 () Real)
+(assert (and (> 0.0 r37) (> r37 (ufrr5 0.0 1.0 1.0 r5 1.0)) (= 0.0 (+ (- 1) (* r6 r58 (- 1))))))
+(assert (= 0.0 (/ 1.0 r5)))
+(check-sat)
--- /dev/null
+(set-logic QF_AUFLRA)
+(set-info :status sat)
+(declare-fun f (Bool Bool Bool Bool Bool) Bool)
+(declare-fun v () Bool)
+(declare-fun r () Real)
+(declare-fun r5 () Real)
+(declare-fun -6 () (Array Real Real))
+(declare-fun -9 () (Array Bool (Array Real Real)))
+(assert (f true v true false false))
+(assert (= (store -9 true -6) (store -9 false (store -6 r5 0))))
+(assert (distinct r r5 (select -6 r)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic QF_ALIA)
+(set-info :status sat)
+(declare-fun i2 () Int)
+(declare-fun arr0 () (Array Int Bool))
+(declare-fun i10 () Int)
+(assert (select (store (store arr0 1 true) i10 false) i2))
+(push)
+(assert (= i10 0))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_ALIA)
+(declare-fun v0 () Bool)
+(declare-fun i1 () Int)
+(declare-fun arr0 () (Array Int Bool))
+(assert (select (store arr0 0 v0) i1))
+(push)
+(assert (= 1 i1))
+(check-sat)
+(check-sat)
; COMMAND-LINE: --incremental --abstract-values
; EXPECT: sat
-; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int))))
+; EXPECT: ((a (as @a_1 (Array Int Int))) (b (as @a_2 (Array Int Int))))
(set-logic QF_AUFLIA)
(set-option :produce-models true)
(declare-fun a () (Array Int Int))
;
; COMMAND-LINE: --incremental --abstract-values --check-models
; EXPECT: sat
-; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int))))
+; EXPECT: ((a (as @a_1 (Array Int Int))) (b (as @a_2 (Array Int Int))))
(set-logic QF_AUFLIA)
(set-option :produce-models true)
(declare-fun a () (Array Int Int))
d_cnfContext.reset(new context::Context());
d_cnfRegistrar.reset(new prop::NullRegistrar);
d_cnfStream.reset(
- new cvc5::prop::CnfStream(d_satSolver.get(),
+ new cvc5::prop::CnfStream(d_slvEngine->getEnv(),
+ d_satSolver.get(),
d_cnfRegistrar.get(),
- d_cnfContext.get(),
- &d_slvEngine->getEnv(),
- d_slvEngine->getResourceManager()));
+ d_cnfContext.get()));
}
void TearDown() override
projects / cvc5.git / commitdiff