Searched refs:isAssumption (Results 1 – 13 of 13) sorted by relevance
38 void AssertionPipeline::push_back(Node n, bool isAssumption) in push_back() argument41 if (isAssumption) in push_back()
58 void push_back(Node n, bool isAssumption = false);
162 virtual bool isAssumption(const Expr& e) = 0;
403 virtual bool isAssumption(const Expr& e);
247 virtual bool isAssumption(const Expr& e);
283 virtual bool isAssumption(const Expr& e);
490 bool Constraint::isAssumption() const { in isAssumption() function in CVC4::theory::arith::Constraint1120 Assert(!isAssumption()); in tryToPropagate()1123 if(canBePropagated() && !assertedToTheTheory() && !isAssumption() && !isInternalAssumption()){ in tryToPropagate()1132 Assert(!isAssumption()); in propagate()1440 Assert(!isAssumption() || assertedToTheTheory()); in externalExplain()1455 Assert(!isAssumption()); in externalExplain()1470 Assert(!isAssumption() || assertedBefore(order)); in externalExplain()1488 Assert(!isAssumption()); in externalExplain()
485 bool isAssumption() const;590 Assert(!isAssumption()); in externalExplainForPropagation()
1988 if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){ in constraintFromFactQueue()1998 if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){ in constraintFromFactQueue()4067 Assert(!c->isAssumption()); in explain()4073 if(!c->isAssumption()){ in explain()
1073 if (!isAssumption(e)) { in newUserAssumptionInt()1163 bool SearchSat::isAssumption(const Expr& e) in isAssumption() function in SearchSat
1594 SearchEngineFast::isAssumption(const Expr& e) { in isAssumption() function in SearchEngineFast1595 return (SearchImplBase::isAssumption(e) in isAssumption()
213 bool SearchImplBase::isAssumption(const Expr& e) { in isAssumption() function in SearchImplBase
781 bool isAssumption = false);3534 bool isAssumption) in addFormula() argument3544 << ", isAssumption = " << isAssumption << endl; in addFormula()3567 d_assertions.push_back(n, isAssumption); in addFormula()