diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-15 03:58:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-15 01:58:54 -0700 |
commit | eb58f1ef8917c5d57d64c54f9188b0ed489b47c1 (patch) | |
tree | c7d4fc304f72dc06b10f052ecf29d5f629fc0193 /src/theory/arith/theory_arith.cpp | |
parent | a932b4478e397d760d9457be7c6a80f9ba724391 (diff) |
Simplify entailment check interface (#4744)
The generality of this interface is unnecessary.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 38 |
1 files changed, 5 insertions, 33 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 83ae5a032..eb5bf3685 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -166,40 +166,12 @@ Node TheoryArith::getModelValue(TNode var) { return d_internal->getModelValue( var ); } - -std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out) +std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit) { - const ArithEntailmentCheckParameters* aparams = NULL; - if(params == NULL){ - ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters(); - def->addLookupRowSumAlgorithms(); - aparams = def; - }else{ - AlwaysAssert(params->getTheoryId() == getId()); - aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params); - } - Assert(aparams != NULL); - - ArithEntailmentCheckSideEffects* ase = NULL; - if(out == NULL){ - ase = new ArithEntailmentCheckSideEffects(); - }else{ - AlwaysAssert(out->getTheoryId() == getId()); - ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out); - } - Assert(ase != NULL); - - std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase); - - if(params == NULL){ - delete aparams; - } - if(out == NULL){ - delete ase; - } - + ArithEntailmentCheckParameters def; + def.addLookupRowSumAlgorithms(); + ArithEntailmentCheckSideEffects ase; + std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase); return res; } |