This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.
: d_ta(ta)
{}
-void RaiseConflict::raiseConflict(ConstraintCP c) const{
+void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
Assert(c->inConflict());
- d_ta.raiseConflict(c);
+ d_ta.raiseConflict(c, id);
}
FarkasConflictBuilder::FarkasConflictBuilder()
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
#include "theory/arith/constraint_forward.h"
+#include "theory/inference_id.h"
#include "util/rational.h"
namespace CVC4 {
RaiseConflict(TheoryArithPrivate& ta);
/** Calls d_ta.raiseConflict(c) */
- void raiseConflict(ConstraintCP c) const;
+ void raiseConflict(ConstraintCP c, InferenceId id) const;
};
class FarkasConflictBuilder {
if(cons->negationHasProof()){
Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
cons->impliedByUnate(ant, true);
- d_raiseConflict.raiseConflict(cons);
+ d_raiseConflict.raiseConflict(cons, InferenceId::UNKNOWN);
return true;
}else if(!cons->isTrue()){
++d_statistics.d_unatePropagateImplications;
void NonlinearExtension::check(Theory::Effort e)
{
+ d_im.reset();
Trace("nl-ext") << std::endl;
Trace("nl-ext") << "NonlinearExtension::check, effort = " << e
<< ", built model = " << d_builtModel.get() << std::endl;
d_im.doPendingFacts();
d_im.doPendingLemmas();
d_im.doPendingPhaseRequirements();
- d_im.reset();
return;
}
// Otherwise, we will answer SAT. The values that we approximated are
ConstraintCP conflicted = generateConflictForBasic(basic);
Assert(conflicted != NullConstraint);
- d_conflictChannel.raiseConflict(conflicted);
+ d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
d_conflictVariables.add(basic);
}
bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
if(checkBasicForConflict(basic)){
ConstraintCP conflicted = generateConflictForBasic(basic);
- d_conflictChannel.raiseConflict(conflicted);
+ d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
return true;
}else{
return false;
d_conflictBuilder->addConstraint(c, coeff);
}
ConstraintCP conflicted = d_conflictBuilder->commitConflict();
- d_conflictChannel.raiseConflict(conflicted);
+ d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
}
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
d_ppPfGen(pnm, c, "Arith::ppRewrite"),
d_astate(*d_internal, c, u, valuation),
- d_inferenceManager(*this, d_astate, pnm),
+ d_im(*this, d_astate, pnm),
d_nonlinearExtension(nullptr),
- d_arithPreproc(d_astate, d_inferenceManager, pnm, logicInfo)
+ d_arithPreproc(d_astate, d_im, pnm, logicInfo)
{
smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
// indicate we are using the theory state object and inference manager
d_theoryState = &d_astate;
- d_inferManager = &d_inferenceManager;
+ d_inferManager = &d_im;
}
TheoryArith::~TheoryArith(){
else if (d_internal->foundNonlinear())
{
// set incomplete
- d_inferenceManager.setIncomplete();
+ d_im.setIncomplete();
}
}
}
{
Node eq = p.first.eqNode(p.second);
Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
- d_out->lemma(lem);
+ d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
}
return false;
}
}
eq::ProofEqEngine* TheoryArith::getProofEqEngine()
{
- return d_inferenceManager.getProofEqEngine();
+ return d_im.getProofEqEngine();
}
}/* CVC4::theory::arith namespace */
/** Return a reference to the arith::InferenceManager. */
InferenceManager& getInferenceManager()
{
- return d_inferenceManager;
+ return d_im;
}
private:
/** The state object wrapping TheoryArithPrivate */
ArithState d_astate;
/** The arith::InferenceManager. */
- InferenceManager d_inferenceManager;
+ InferenceManager d_im;
/**
* The non-linear extension, responsible for all approaches for non-linear
return d_pnm != nullptr;
}
-void TheoryArithPrivate::raiseConflict(ConstraintCP a){
+void TheoryArithPrivate::raiseConflict(ConstraintCP a, InferenceId id){
Assert(a->inConflict());
- d_conflicts.push_back(a);
+ d_conflicts.push_back(std::make_pair(a, id));
}
void TheoryArithPrivate::raiseBlackBoxConflict(Node bb,
ConstraintP negation = constraint->getNegation();
negation->impliedByUnate(ubc, true);
- raiseConflict(constraint);
+ raiseConflict(constraint, InferenceId::ARITH_CONF_LOWER);
++(d_statistics.d_statAssertLowerConflicts);
return true;
}
if(triConflict){
++(d_statistics.d_statDisequalityConflicts);
- raiseConflict(eq);
+ raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY);
return true;
}
}
negUb->tryToPropagate();
}
if(ubInConflict){
- raiseConflict(ub);
+ raiseConflict(ub, InferenceId::ARITH_CONF_TRICHOTOMY);
return true;
}else if(learnNegUb){
d_learnedBounds.push_back(negUb);
ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
ConstraintP negConstraint = constraint->getNegation();
negConstraint->impliedByUnate(lbc, true);
- raiseConflict(constraint);
+ raiseConflict(constraint, InferenceId::ARITH_CONF_UPPER);
++(d_statistics.d_statAssertUpperConflicts);
return true;
}else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
}
if(triConflict){
++(d_statistics.d_statDisequalityConflicts);
- raiseConflict(eq);
+ raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY);
return true;
}
}
negLb->tryToPropagate();
}
if(lbInConflict){
- raiseConflict(lb);
+ raiseConflict(lb, InferenceId::ARITH_CONF_TRICHOTOMY);
return true;
}else if(learnNegLb){
d_learnedBounds.push_back(negLb);
ConstraintP diseq = constraint->getNegation();
Assert(!diseq->isTrue());
diseq->impliedByUnate(cb, true);
- raiseConflict(constraint);
+ raiseConflict(constraint, InferenceId::ARITH_CONF_EQ);
return true;
}
if(lb->isTrue() && ub->isTrue()){
ConstraintP eq = constraint->getNegation();
eq->impliedByTrichotomy(lb, ub, true);
- raiseConflict(constraint);
+ raiseConflict(constraint, InferenceId::ARITH_CONF_TRICHOTOMY);
//in conflict
++(d_statistics.d_statDisequalityConflicts);
return true;
if(!split && c_i == d_partialModel.getAssignment(x_i)){
Debug("arith::eq") << "lemma now! " << constraint << endl;
- outputTrustedLemma(constraint->split());
+ outputTrustedLemma(constraint->split(), InferenceId::ARITH_SPLIT_DEQ);
return false;
}else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
Debug("arith::eq") << "can drop as less than lb" << constraint << endl;
Debug("arith::eq") << "negation has proof" << endl;
Debug("arith::eq") << constraint << endl;
Debug("arith::eq") << negation << endl;
- raiseConflict(negation);
+ raiseConflict(negation, InferenceId::UNKNOWN);
return NullConstraint;
}else{
return constraint;
floorConstraint->impliedByIntTighten(constraint, inConflict);
floorConstraint->tryToPropagate();
if(inConflict){
- raiseConflict(floorConstraint);
+ raiseConflict(floorConstraint, InferenceId::ARITH_TIGHTEN_FLOOR);
return true;
}
}
ceilingConstraint->impliedByIntTighten(constraint, inConflict);
ceilingConstraint->tryToPropagate();
if(inConflict){
- raiseConflict(ceilingConstraint);
+ raiseConflict(ceilingConstraint, InferenceId::ARITH_TIGHTEN_CEIL);
return true;
}
}
if(!conflictQueueEmpty()){
Assert(!d_conflicts.empty());
for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
- ConstraintCP confConstraint = d_conflicts[i];
+ const std::pair<ConstraintCP, InferenceId>& conf = d_conflicts[i];
+ const ConstraintCP& confConstraint = conf.first;
bool hasProof = confConstraint->hasProof();
Assert(confConstraint->inConflict());
const ConstraintRule& pf = confConstraint->getConstraintRule();
if (isProofEnabled())
{
- outputTrustedConflict(trustedConflict);
+ outputTrustedConflict(trustedConflict, conf.second);
}
else
{
- outputConflict(conflict);
+ outputConflict(conflict, conf.second);
}
}
}
if (isProofEnabled() && d_blackBoxConflictPf.get())
{
auto confPf = d_blackBoxConflictPf.get();
- outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true));
+ outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true), InferenceId::ARITH_BLACK_BOX);
}
else
{
- outputConflict(bb);
+ outputConflict(bb, InferenceId::ARITH_BLACK_BOX);
}
}
}
-void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma)
+void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
{
Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl;
- (d_containing.d_out)->trustedLemma(lemma);
+ d_containing.d_im.trustedLemma(lemma, id);
}
-void TheoryArithPrivate::outputLemma(TNode lem) {
+void TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
Debug("arith::channel") << "Arith lemma: " << lem << std::endl;
- (d_containing.d_out)->lemma(lem);
+ d_containing.d_im.lemma(lem, id);
}
-void TheoryArithPrivate::outputTrustedConflict(TrustNode conf)
+void TheoryArithPrivate::outputTrustedConflict(TrustNode conf, InferenceId id)
{
Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl;
- (d_containing.d_out)->trustedConflict(conf);
+ d_containing.d_im.trustedConflict(conf, id);
}
-void TheoryArithPrivate::outputConflict(TNode lit) {
+void TheoryArithPrivate::outputConflict(TNode lit, InferenceId id) {
Debug("arith::channel") << "Arith conflict: " << lit << std::endl;
- (d_containing.d_out)->conflict(lit);
+ d_containing.d_im.conflict(lit, id);
}
void TheoryArithPrivate::outputPropagate(TNode lit) {
Debug("arith::channel") << "Arith propagation: " << lit << std::endl;
// call the propagate lit method of the
- (d_containing.d_out)->propagate(lit);
+ d_containing.d_im.propagateLit(lit);
}
void TheoryArithPrivate::outputRestart() {
<< " (" << neg_at_j->isTrue() <<") " << neg_at_j << endl
<< " (" << at_j->isTrue() <<") " << at_j << endl;
neg_at_j->impliedByIntHole(vec, true);
- raiseConflict(at_j);
+ raiseConflict(at_j, InferenceId::UNKNOWN);
break;
}
}
for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
conflicts.push_back(ConstraintCPVec());
- intHoleConflictToVector(d_conflicts[i], conflicts.back());
+ intHoleConflictToVector(d_conflicts[i].first, conflicts.back());
Constraint::assertionFringe(conflicts.back());
// ConstraintCP conflicting = d_conflicts[i];
if(!contains(conf, bcneg)){
Debug("approx::branch") << "reraise " << conf << endl;
ConstraintCP conflicting = vectorToIntHoleConflict(conf);
- raiseConflict(conflicting);
+ raiseConflict(conflicting, InferenceId::UNKNOWN);
}else if(!bci.proven()){
drop(conf, bcneg);
bci.setExplanation(conf);
}
Debug("approx::replayAssert") << "replayAssertion " << c << endl;
if(inConflict){
- raiseConflict(c);
+ raiseConflict(c, InferenceId::UNKNOWN);
}else{
assertionCases(c);
}
}else {
con->impliedByIntHole(exp, true);
Debug("approx::replayLogRec") << "cut into conflict " << con << endl;
- raiseConflict(con);
+ raiseConflict(con, InferenceId::UNKNOWN);
}
}else{
++d_statistics.d_cutsProofFailed;
/* if a conflict has been found stop */
for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
res.push_back(ConstraintCPVec());
- intHoleConflictToVector(d_conflicts[i], res.back());
+ intHoleConflictToVector(d_conflicts[i].first, res.back());
}
++d_statistics.d_replayLogRecEarlyExit;
}else if(nl.isBranch()){
Debug("arith::approx::cuts") << "approximate cut:" << lem << endl;
anyFresh = anyFresh || hasFreshArithLiteral(lem.getNode());
Debug("arith::lemma") << "approximate cut:" << lem << endl;
- outputTrustedLemma(lem);
+ outputTrustedLemma(lem, InferenceId::ARITH_APPROX_CUT);
}
if(anyFresh){
emmittedConflictOrSplit = true;
d_hasDoneWorkSinceCut = false;
d_cutCount = d_cutCount + 1;
Debug("arith::lemma") << "dio cut " << possibleLemma << endl;
- outputTrustedLemma(possibleLemma);
+ outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT);
}
}
}
emmittedConflictOrSplit = true;
Debug("arith::lemma") << "rrbranch lemma"
<< possibleLemma << endl;
- outputTrustedLemma(possibleLemma);
+ outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA);
}
}
Node decompositionLemma = d_diosolver.nextDecompositionLemma();
Debug("arith::lemma") << "dio decomposition lemma "
<< decompositionLemma << endl;
- outputLemma(decompositionLemma);
+ outputLemma(decompositionLemma, InferenceId::ARITH_DIO_DECOMPOSITION);
}
}else{
Debug("arith::restart") << "arith restart!" << endl;
Debug("arith::lemma")
<< "Now " << Rewriter::rewrite(lemma.getNode()) << endl;
- outputTrustedLemma(lemma);
+ outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ);
//cout << "Now " << Rewriter::rewrite(lemma) << endl;
splitSomething = true;
}else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
for(; i != i_end; ++i){
TrustNode lem = *i;
Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
- outputTrustedLemma(lem);
+ outputTrustedLemma(lem, InferenceId::UNKNOWN);
}
}
// Output it
TrustNode trustedClause = d_pfGen->mkTrustNode(clause, clausePf);
- outputTrustedLemma(trustedClause);
+ outputTrustedLemma(trustedClause, InferenceId::UNKNOWN);
}
else
{
- outputLemma(clause);
+ outputLemma(clause, InferenceId::UNKNOWN);
}
}else{
Assert(!implied->negationHasProof());
/** This is only used by simplex at the moment. */
- context::CDList<ConstraintCP> d_conflicts;
+ context::CDList<std::pair<ConstraintCP, InferenceId>> d_conflicts;
/** This is only used by simplex at the moment. */
context::CDO<Node> d_blackBoxConflict;
* This adds the constraint a to the queue of conflicts in d_conflicts.
* Both a and ~a must have a proof.
*/
- void raiseConflict(ConstraintCP a);
+ void raiseConflict(ConstraintCP a, InferenceId id);
// inline void raiseConflict(const ConstraintCPVec& cv){
// d_conflicts.push_back(cv);
inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); }
inline void debugPrintFacts() const { d_containing.debugPrintFacts(); }
inline context::Context* getSatContext() const { return d_containing.getSatContext(); }
- void outputTrustedLemma(TrustNode lem);
- void outputLemma(TNode lem);
- void outputTrustedConflict(TrustNode conf);
- void outputConflict(TNode lit);
+ void outputTrustedLemma(TrustNode lem, InferenceId id);
+ void outputLemma(TNode lem, InferenceId id);
+ void outputTrustedConflict(TrustNode conf, InferenceId id);
+ void outputConflict(TNode lit, InferenceId id);
void outputPropagate(TNode lit);
void outputRestart();
enum class InferenceId
{
// ---------------------------------- arith theory
+ //-------------------- linear core
+ // black box conflicts. It's magic.
+ ARITH_BLACK_BOX,
+ // conflicting equality
+ ARITH_CONF_EQ,
+ // conflicting lower bound
+ ARITH_CONF_LOWER,
+ // conflict due to trichotomy
+ ARITH_CONF_TRICHOTOMY,
+ // conflicting upper bound
+ ARITH_CONF_UPPER,
+ // introduces split on a disequality
+ ARITH_SPLIT_DEQ,
+ // tighten integer inequalities to ceiling
+ ARITH_TIGHTEN_CEIL,
+ // tighten integer inequalities to floor
+ ARITH_TIGHTEN_FLOOR,
+ ARITH_APPROX_CUT,
+ ARITH_BB_LEMMA,
+ ARITH_DIO_CUT,
+ ARITH_DIO_DECOMPOSITION,
+ ARITH_SPLIT_FOR_NL_MODEL,
//-------------------- preprocessing
// equivalence of term and its preprocessed form
ARITH_PP_ELIM_OPERATORS,
return d_userContext;
}
- /**
- * Set the output channel associated to this theory.
- */
- void setOutputChannel(OutputChannel& out) {
- d_out = &out;
- }
-
/**
* Get the output channel associated to this theory.
*/
TestSmtNoFinishInit::SetUp();
d_smtEngine->setOption("incremental", "false");
d_smtEngine->finishInit();
- d_context = d_smtEngine->getContext();
- d_user_context = d_smtEngine->getUserContext();
- d_outputChannel.clear();
- d_logicInfo.lock();
- d_smtEngine->getTheoryEngine()
- ->d_theoryTable[THEORY_ARITH]
- ->setOutputChannel(d_outputChannel);
d_arith = static_cast<TheoryArith*>(
d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
- d_preregistered.reset(new std::set<Node>());
-
- d_booleanType.reset(new TypeNode(d_nodeManager->booleanType()));
d_realType.reset(new TypeNode(d_nodeManager->realType()));
d_intType.reset(new TypeNode(d_nodeManager->integerType()));
}
void fakeTheoryEnginePreprocess(TNode input)
{
Assert(input == Rewriter::rewrite(input));
- Node rewrite = input;
- if (d_debug)
- {
- std::cout << "input " << input << " rewrite " << rewrite << std::endl;
- }
-
- std::list<Node> toPreregister;
-
- toPreregister.push_back(rewrite);
- for (std::list<Node>::iterator i = toPreregister.begin();
- i != toPreregister.end();
- ++i)
- {
- Node n = *i;
- d_preregistered->insert(n);
-
- for (Node::iterator citer = n.begin(); citer != n.end(); ++citer)
- {
- Node c = *citer;
- if (d_preregistered->find(c) == d_preregistered->end())
- {
- toPreregister.push_back(c);
- }
- }
- }
- for (std::list<Node>::reverse_iterator i = toPreregister.rbegin();
- i != toPreregister.rend();
- ++i)
- {
- Node n = *i;
- if (d_debug)
- {
- std::cout << "id " << n.getId() << " " << n << std::endl;
- }
- d_arith->preRegisterTerm(n);
- }
+ d_smtEngine->getTheoryEngine()->preRegister(input);
}
- Context* d_context;
- UserContext* d_user_context;
- DummyOutputChannel d_outputChannel;
- LogicInfo d_logicInfo;
Theory::Effort d_level = Theory::EFFORT_FULL;
TheoryArith* d_arith;
- std::unique_ptr<std::set<Node>> d_preregistered;
- std::unique_ptr<TypeNode> d_booleanType;
std::unique_ptr<TypeNode> d_realType;
std::unique_ptr<TypeNode> d_intType;
const Rational d_zero = 0;
const Rational d_one = 1;
- bool d_debug = false;
};
TEST_F(TestTheoryWhiteArith, assert)
d_arith->assertFact(leq, true);
d_arith->check(d_level);
-
- ASSERT_EQ(d_outputChannel.getNumCalls(), 0u);
-}
-
-TEST_F(TestTheoryWhiteArith, TPLt1)
-{
- Node x = d_nodeManager->mkVar(*d_realType);
- Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
- Node c1 = d_nodeManager->mkConst<Rational>(d_one);
-
- Node gt0 = d_nodeManager->mkNode(GT, x, c0);
- Node gt1 = d_nodeManager->mkNode(GT, x, c1);
- Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
- Node leq0 = Rewriter::rewrite(gt0.notNode());
- Node leq1 = Rewriter::rewrite(gt1.notNode());
- Node lt1 = Rewriter::rewrite(geq1.notNode());
-
- fakeTheoryEnginePreprocess(leq0);
- fakeTheoryEnginePreprocess(leq1);
- fakeTheoryEnginePreprocess(geq1);
-
- d_arith->presolve();
- d_arith->assertFact(lt1, true);
- d_arith->check(d_level);
- d_arith->propagate(d_level);
-
- Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
- Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
- geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
-
- std::cout << d_outputChannel.getIthNode(0) << std::endl << std::endl;
- std::cout << d_outputChannel.getIthNode(1) << std::endl << std::endl;
- std::cout << d_outputChannel.getIthNode(2) << std::endl << std::endl;
-
- ASSERT_EQ(d_outputChannel.getNumCalls(), 3u);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
- ASSERT_TRUE(d_outputChannel.getIthNode(0) == gt0OrLt1);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
- ASSERT_TRUE(d_outputChannel.getIthNode(1) == geq0OrLeq1);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE);
- ASSERT_EQ(d_outputChannel.getIthNode(2), leq1);
-}
-
-TEST_F(TestTheoryWhiteArith, TPLeq0)
-{
- Node x = d_nodeManager->mkVar(*d_realType);
- Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
- Node c1 = d_nodeManager->mkConst<Rational>(d_one);
-
- Node gt0 = d_nodeManager->mkNode(GT, x, c0);
- Node gt1 = d_nodeManager->mkNode(GT, x, c1);
- Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
- Node leq0 = Rewriter::rewrite(gt0.notNode());
- Node leq1 = Rewriter::rewrite(gt1.notNode());
- Node lt1 = Rewriter::rewrite(geq1.notNode());
-
- fakeTheoryEnginePreprocess(leq0);
- fakeTheoryEnginePreprocess(leq1);
- fakeTheoryEnginePreprocess(geq1);
-
- d_arith->presolve();
- d_arith->assertFact(leq0, true);
- d_arith->check(d_level);
- d_arith->propagate(d_level);
-
- Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
- Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
- geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
-
- std::cout << d_outputChannel.getIthNode(0) << std::endl;
- std::cout << d_outputChannel.getIthNode(1) << std::endl;
- std::cout << d_outputChannel.getIthNode(2) << std::endl;
- std::cout << d_outputChannel.getIthNode(3) << std::endl;
-
- ASSERT_EQ(d_outputChannel.getNumCalls(), 4u);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
- ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
- ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE);
- ASSERT_EQ(d_outputChannel.getIthNode(2), lt1);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(3), PROPAGATE);
- ASSERT_EQ(d_outputChannel.getIthNode(3), leq1);
-}
-
-TEST_F(TestTheoryWhiteArith, TPLeq1)
-{
- Node x = d_nodeManager->mkVar(*d_realType);
- Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
- Node c1 = d_nodeManager->mkConst<Rational>(d_one);
-
- Node gt0 = d_nodeManager->mkNode(GT, x, c0);
- Node gt1 = d_nodeManager->mkNode(GT, x, c1);
- Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
- Node leq0 = Rewriter::rewrite(gt0.notNode());
- Node leq1 = Rewriter::rewrite(gt1.notNode());
- Node lt1 = Rewriter::rewrite(geq1.notNode());
-
- fakeTheoryEnginePreprocess(leq0);
- fakeTheoryEnginePreprocess(leq1);
- fakeTheoryEnginePreprocess(geq1);
-
- d_arith->presolve();
- d_arith->assertFact(leq1, true);
- d_arith->check(d_level);
- d_arith->propagate(d_level);
-
- Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
- Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
- geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
-
- std::cout << d_outputChannel.getIthNode(0) << std::endl;
- std::cout << d_outputChannel.getIthNode(1) << std::endl;
-
- ASSERT_EQ(d_outputChannel.getNumCalls(), 2u);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
- ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1);
-
- ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
- ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1);
}
TEST_F(TestTheoryWhiteArith, int_normal_form)
ASSERT_TRUE(d_dummy_theory->done());
}
-TEST_F(TestTheoryWhite, outputChannel_accessors)
-{
- /* void setOutputChannel(OutputChannel& out) */
- /* OutputChannel& getOutputChannel() */
-
- DummyOutputChannel theOtherChannel;
-
- ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &d_outputChannel);
-
- d_dummy_theory->setOutputChannel(theOtherChannel);
-
- ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &theOtherChannel);
-
- const OutputChannel& oc = d_dummy_theory->getOutputChannel();
-
- ASSERT_EQ(&oc, &theOtherChannel);
-}
-
TEST_F(TestTheoryWhite, outputChannel)
{
Node n = d_atom0.orNode(d_atom1);
projects / cvc5.git / commitdiff