summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/theory/arith/callbacks.cpp43
-rw-r--r--src/theory/arith/callbacks.h6
-rw-r--r--src/theory/arith/constraint.cpp149
-rw-r--r--src/theory/arith/constraint.h81
-rw-r--r--src/theory/arith/linear_equality.cpp6
-rw-r--r--src/theory/arith/linear_equality.h161
-rw-r--r--src/theory/arith/proof_macros.h32
-rw-r--r--src/theory/arith/simplex.cpp3
-rw-r--r--src/theory/arith/theory_arith_private.cpp19
10 files changed, 255 insertions, 246 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8053340e8..5dbaa3349 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -509,7 +509,6 @@ libcvc5_add_sources(
theory/arith/pp_rewrite_eq.h
theory/arith/proof_checker.cpp
theory/arith/proof_checker.h
- theory/arith/proof_macros.h
theory/arith/rewrites.cpp
theory/arith/rewrites.h
theory/arith/simplex.cpp
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 0c0a4959d..5b529ab7d 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -20,7 +20,6 @@
#include "expr/skolem_manager.h"
#include "proof/proof_node.h"
-#include "theory/arith/proof_macros.h"
#include "theory/arith/theory_arith_private.h"
namespace cvc5 {
@@ -73,11 +72,12 @@ void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
d_ta.raiseConflict(c, id);
}
-FarkasConflictBuilder::FarkasConflictBuilder()
- : d_farkas()
- , d_constraints()
- , d_consequent(NullConstraint)
- , d_consequentSet(false)
+FarkasConflictBuilder::FarkasConflictBuilder(bool produceProofs)
+ : d_farkas(),
+ d_constraints(),
+ d_consequent(NullConstraint),
+ d_consequentSet(false),
+ d_produceProofs(produceProofs)
{
reset();
}
@@ -94,17 +94,20 @@ void FarkasConflictBuilder::reset(){
d_consequent = NullConstraint;
d_constraints.clear();
d_consequentSet = false;
- ARITH_PROOF(d_farkas.clear());
+ if (d_produceProofs)
+ {
+ d_farkas.clear();
+ }
Assert(!underConstruction());
}
/* Adds a constraint to the constraint under construction. */
void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
Assert(
- !ARITH_PROOF_ON()
+ !d_produceProofs
|| (!underConstruction() && d_constraints.empty() && d_farkas.empty())
|| (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
- Assert(ARITH_PROOF_ON() || d_farkas.empty());
+ Assert(d_produceProofs || d_farkas.empty());
Assert(c->isTrue());
if(d_consequent == NullConstraint){
@@ -112,14 +115,17 @@ void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
} else {
d_constraints.push_back(c);
}
- ARITH_PROOF(d_farkas.push_back(fc));
- Assert(!ARITH_PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
- Assert(ARITH_PROOF_ON() || d_farkas.empty());
+ if (d_produceProofs)
+ {
+ d_farkas.push_back(fc);
+ }
+ Assert(!d_produceProofs || d_constraints.size() + 1 == d_farkas.size());
+ Assert(d_produceProofs || d_farkas.empty());
}
void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
Assert(!mult.isZero());
- if (ARITH_PROOF_ON() && !mult.isOne())
+ if (d_produceProofs && !mult.isOne())
{
Rational prod = fc * mult;
addConstraint(c, prod);
@@ -142,7 +148,10 @@ void FarkasConflictBuilder::makeLastConsequent(){
ConstraintCP last = d_constraints.back();
d_constraints.back() = d_consequent;
d_consequent = last;
- ARITH_PROOF(std::swap(d_farkas.front(), d_farkas.back()));
+ if (d_produceProofs)
+ {
+ std::swap(d_farkas.front(), d_farkas.back());
+ }
d_consequentSet = true;
}
@@ -155,14 +164,14 @@ ConstraintCP FarkasConflictBuilder::commitConflict(){
Assert(underConstruction());
Assert(!d_constraints.empty());
Assert(
- !ARITH_PROOF_ON()
+ !d_produceProofs
|| (!underConstruction() && d_constraints.empty() && d_farkas.empty())
|| (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
- Assert(ARITH_PROOF_ON() || d_farkas.empty());
+ Assert(d_produceProofs || d_farkas.empty());
Assert(d_consequentSet);
ConstraintP not_c = d_consequent->getNegation();
- RationalVectorCP coeffs = ARITH_NULLPROOF(&d_farkas);
+ RationalVectorCP coeffs = d_produceProofs ? &d_farkas : nullptr;
not_c->impliedByFarkas(d_constraints, coeffs, true );
reset();
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index c8249a9fc..049b621c3 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -122,12 +122,14 @@ private:
ConstraintCPVec d_constraints;
ConstraintCP d_consequent;
bool d_consequentSet;
-public:
+ bool d_produceProofs;
+
+ public:
/**
* Constructs a new FarkasConflictBuilder.
*/
- FarkasConflictBuilder();
+ FarkasConflictBuilder(bool produceProofs);
/**
* Adds an antecedent constraint to the conflict under construction
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 03db36bb5..defcc8aff 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -22,8 +22,10 @@
#include <unordered_set>
#include "base/output.h"
+#include "options/smt_options.h"
#include "proof/eager_proof_generator.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/congruence_manager.h"
@@ -39,6 +41,37 @@ namespace cvc5 {
namespace theory {
namespace arith {
+ConstraintRule::ConstraintRule()
+ : d_constraint(NullConstraint),
+ d_proofType(NoAP),
+ d_antecedentEnd(AntecedentIdSentinel)
+{
+ d_farkasCoefficients = RationalVectorCPSentinel;
+}
+
+ConstraintRule::ConstraintRule(ConstraintP con, ArithProofType pt)
+ : d_constraint(con), d_proofType(pt), d_antecedentEnd(AntecedentIdSentinel)
+{
+ d_farkasCoefficients = RationalVectorCPSentinel;
+}
+ConstraintRule::ConstraintRule(ConstraintP con,
+ ArithProofType pt,
+ AntecedentId antecedentEnd)
+ : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
+{
+ d_farkasCoefficients = RationalVectorCPSentinel;
+}
+
+ConstraintRule::ConstraintRule(ConstraintP con,
+ ArithProofType pt,
+ AntecedentId antecedentEnd,
+ RationalVectorCP coeffs)
+ : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
+{
+ Assert(con->isProofProducing() || coeffs == RationalVectorCPSentinel);
+ d_farkasCoefficients = coeffs;
+}
+
/** Given a simplifiedKind this returns the corresponding ConstraintType. */
//ConstraintType constraintTypeOfLiteral(Kind k);
ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
@@ -72,19 +105,23 @@ ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
}
}
-Constraint::Constraint(ArithVar x, ConstraintType t, const DeltaRational& v)
- : d_variable(x),
- d_type(t),
- d_value(v),
- d_database(NULL),
- d_literal(Node::null()),
- d_negation(NullConstraint),
- d_canBePropagated(false),
- d_assertionOrder(AssertionOrderSentinel),
- d_witness(TNode::null()),
- d_crid(ConstraintRuleIdSentinel),
- d_split(false),
- d_variablePosition()
+Constraint::Constraint(ArithVar x,
+ ConstraintType t,
+ const DeltaRational& v,
+ bool produceProofs)
+ : d_variable(x),
+ d_type(t),
+ d_value(v),
+ d_database(NULL),
+ d_literal(Node::null()),
+ d_negation(NullConstraint),
+ d_canBePropagated(false),
+ d_assertionOrder(AssertionOrderSentinel),
+ d_witness(TNode::null()),
+ d_crid(ConstraintRuleIdSentinel),
+ d_split(false),
+ d_variablePosition(),
+ d_produceProofs(produceProofs)
{
Assert(!initialized());
}
@@ -542,7 +579,7 @@ bool Constraint::hasSimpleFarkasProof() const
{
Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there "
"is an antecdent w/ rule ";
- a->getConstraintRule().print(Debug("constraints::hsfp"));
+ a->getConstraintRule().print(Debug("constraints::hsfp"), d_produceProofs);
Debug("constraints::hsfp") << std::endl;
}
@@ -576,7 +613,7 @@ bool Constraint::hasTrichotomyProof() const {
void Constraint::printProofTree(std::ostream& out, size_t depth) const
{
- if (ARITH_PROOF_ON())
+ if (d_produceProofs)
{
const ConstraintRule& rule = getConstraintRule();
out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
@@ -662,18 +699,16 @@ bool Constraint::sanityChecking(Node n) const {
}
}
-void ConstraintRule::debugPrint() const {
- print(std::cerr);
-}
+void ConstraintRule::debugPrint() const { print(std::cerr, false); }
ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
Assert(p < d_antecedents.size());
return d_antecedents[p];
}
-
-void ConstraintRule::print(std::ostream& out) const {
- RationalVectorCP coeffs = ARITH_NULLPROOF(d_farkasCoefficients);
+void ConstraintRule::print(std::ostream& out, bool produceProofs) const
+{
+ RationalVectorCP coeffs = produceProofs ? d_farkasCoefficients : nullptr;
out << "{ConstraintRule, ";
out << d_constraint << std::endl;
out << "d_proofType= " << d_proofType << ", " << std::endl;
@@ -724,11 +759,11 @@ bool Constraint::wellFormedFarkasProof() const {
ConstraintCP antecedent = d_database->d_antecedents[p];
if(antecedent == NullConstraint) { return false; }
- if (!ARITH_PROOF_ON())
+ if (!d_produceProofs)
{
return cr.d_farkasCoefficients == RationalVectorCPSentinel;
}
- Assert(ARITH_PROOF_ON());
+ Assert(d_produceProofs);
if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
if(cr.d_farkasCoefficients->size() < 2){ return false; }
@@ -828,7 +863,11 @@ bool Constraint::wellFormedFarkasProof() const {
&& rhs.sgn() < 0;
}
-ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
+ConstraintP Constraint::makeNegation(ArithVar v,
+ ConstraintType t,
+ const DeltaRational& r,
+ bool produceProofs)
+{
switch(t){
case LowerBound:
{
@@ -837,12 +876,12 @@ ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRa
Assert(r.getInfinitesimalPart() == 1);
// make (not (v > r)), which is (v <= r)
DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
- return new Constraint(v, UpperBound, dropInf);
+ return new Constraint(v, UpperBound, dropInf, produceProofs);
}else{
Assert(r.infinitesimalSgn() == 0);
// make (not (v >= r)), which is (v < r)
DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
- return new Constraint(v, UpperBound, addInf);
+ return new Constraint(v, UpperBound, addInf, produceProofs);
}
}
case UpperBound:
@@ -852,40 +891,35 @@ ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRa
Assert(r.getInfinitesimalPart() == -1);
// make (not (v < r)), which is (v >= r)
DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
- return new Constraint(v, LowerBound, dropInf);
+ return new Constraint(v, LowerBound, dropInf, produceProofs);
}else{
Assert(r.infinitesimalSgn() == 0);
// make (not (v <= r)), which is (v > r)
DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
- return new Constraint(v, LowerBound, addInf);
+ return new Constraint(v, LowerBound, addInf, produceProofs);
}
}
- case Equality:
- return new Constraint(v, Disequality, r);
- case Disequality:
- return new Constraint(v, Equality, r);
- default:
- Unreachable();
- return NullConstraint;
+ case Equality: return new Constraint(v, Disequality, r, produceProofs);
+ case Disequality: return new Constraint(v, Equality, r, produceProofs);
+ default: Unreachable(); return NullConstraint;
}
}
-ConstraintDatabase::ConstraintDatabase(context::Context* satContext,
- context::Context* userContext,
+ConstraintDatabase::ConstraintDatabase(Env& env,
const ArithVariables& avars,
ArithCongruenceManager& cm,
RaiseConflict raiseConflict,
- EagerProofGenerator* pfGen,
- ProofNodeManager* pnm)
- : d_varDatabases(),
- d_toPropagate(satContext),
- d_antecedents(satContext, false),
- d_watches(new Watches(satContext, userContext)),
+ EagerProofGenerator* pfGen)
+ : EnvObj(env),
+ d_varDatabases(),
+ d_toPropagate(context()),
+ d_antecedents(context(), false),
+ d_watches(new Watches(context(), userContext())),
d_avariables(avars),
d_congruenceManager(cm),
- d_satContext(satContext),
d_pfGen(pfGen),
- d_pnm(pnm),
+ d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
+ : nullptr),
d_raiseConflict(raiseConflict),
d_one(1),
d_negOne(-1)
@@ -938,8 +972,9 @@ ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, cons
if(vc.hasConstraintOfType(t)){
return vc.getConstraintOfType(t);
}else{
- ConstraintP c = new Constraint(v, t, r);
- ConstraintP negC = Constraint::makeNegation(v, t, r);
+ ConstraintP c = new Constraint(v, t, r, options().smt.produceProofs);
+ ConstraintP negC =
+ Constraint::makeNegation(v, t, r, options().smt.produceProofs);
SortedConstraintMapIterator negPos;
if(t == Equality || t == Disequality){
@@ -1139,7 +1174,8 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
DeltaRational posDR = posCmp.normalizedDeltaRational();
- ConstraintP posC = new Constraint(v, posType, posDR);
+ ConstraintP posC =
+ new Constraint(v, posType, posDR, options().smt.produceProofs);
Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl;
Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
@@ -1170,7 +1206,8 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
DeltaRational negDR = negCmp.normalizedDeltaRational();
- ConstraintP negC = new Constraint(v, negType, negDR);
+ ConstraintP negC =
+ new Constraint(v, negType, negDR, options().smt.produceProofs);
SortedConstraintMapIterator negI;
@@ -1270,7 +1307,7 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
RationalVectorP coeffs;
- if (ARITH_PROOF_ON())
+ if (d_produceProofs)
{
std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
@@ -1294,7 +1331,7 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
}
if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
- getConstraintRule().print(Debug("constraints::wffp"));
+ getConstraintRule().print(Debug("constraints::wffp"), d_produceProofs);
}
Assert(wellFormedFarkasProof());
}
@@ -1418,8 +1455,8 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
Assert(negationHasProof() == nowInConflict);
Assert(allHaveProof(a));
- Assert(ARITH_PROOF_ON() == (coeffs != RationalVectorCPSentinel));
- Assert(!ARITH_PROOF_ON() || coeffs->size() == a.size() + 1);
+ Assert(d_produceProofs == (coeffs != RationalVectorCPSentinel));
+ Assert(!d_produceProofs || coeffs->size() == a.size() + 1);
Assert(a.size() >= 1);
@@ -1432,7 +1469,7 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
RationalVectorCP coeffsCopy;
- if (ARITH_PROOF_ON())
+ if (d_produceProofs)
{
Assert(coeffs != RationalVectorCPSentinel);
coeffsCopy = new RationalVector(*coeffs);
@@ -1448,7 +1485,7 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef
Debug("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl;
}
if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
- getConstraintRule().print(Debug("constraints::wffp"));
+ getConstraintRule().print(Debug("constraints::wffp"), d_produceProofs);
}
Assert(wellFormedFarkasProof());
}
@@ -1661,7 +1698,7 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
{
this->printProofTree(Debug("arith::pf::tree"));
Debug("pf::arith::explain") << "Explaining: " << this << " with rule ";
- getConstraintRule().print(Debug("pf::arith::explain"));
+ getConstraintRule().print(Debug("pf::arith::explain"), d_produceProofs);
Debug("pf::arith::explain") << std::endl;
}
Assert(hasProof());
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index f6306049b..1262181db 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -87,11 +87,11 @@
#include "context/cdqueue.h"
#include "expr/node.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/callbacks.h"
#include "theory/arith/constraint_forward.h"
#include "theory/arith/delta_rational.h"
-#include "theory/arith/proof_macros.h"
#include "util/statistics_stats.h"
namespace cvc5 {
@@ -310,39 +310,18 @@ struct ConstraintRule {
* coefficients.
*/
RationalVectorCP d_farkasCoefficients;
- ConstraintRule()
- : d_constraint(NullConstraint)
- , d_proofType(NoAP)
- , d_antecedentEnd(AntecedentIdSentinel)
- {
- d_farkasCoefficients = RationalVectorCPSentinel;
- }
-
- ConstraintRule(ConstraintP con, ArithProofType pt)
- : d_constraint(con)
- , d_proofType(pt)
- , d_antecedentEnd(AntecedentIdSentinel)
- {
- d_farkasCoefficients = RationalVectorCPSentinel;
- }
- ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd)
- : d_constraint(con)
- , d_proofType(pt)
- , d_antecedentEnd(antecedentEnd)
- {
- d_farkasCoefficients = RationalVectorCPSentinel;
- }
- ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs)
- : d_constraint(con)
- , d_proofType(pt)
- , d_antecedentEnd(antecedentEnd)
- {
- Assert(ARITH_PROOF_ON() || coeffs == RationalVectorCPSentinel);
- d_farkasCoefficients = coeffs;
- }
-
- void print(std::ostream& out) const;
+ ConstraintRule();
+ ConstraintRule(ConstraintP con, ArithProofType pt);
+ ConstraintRule(ConstraintP con,
+ ArithProofType pt,
+ AntecedentId antecedentEnd);
+ ConstraintRule(ConstraintP con,
+ ArithProofType pt,
+ AntecedentId antecedentEnd,
+ RationalVectorCP coeffs);
+
+ void print(std::ostream& out, bool produceProofs) const;
void debugPrint() const;
}; /* class ConstraintRule */
@@ -359,7 +338,10 @@ class Constraint {
* Because of circular dependencies a Constraint is not fully valid until
* initialize has been called on it.
*/
- Constraint(ArithVar x, ConstraintType t, const DeltaRational& v);
+ Constraint(ArithVar x,
+ ConstraintType t,
+ const DeltaRational& v,
+ bool produceProofs);
/**
* Destructor for a constraint.
@@ -492,6 +474,9 @@ class Constraint {
/** Returns true if the node is an assumption.*/
bool isAssumption() const;
+ /** Whether we produce proofs */
+ bool isProofProducing() const { return d_produceProofs; }
+
/** Set the constraint to have an EqualityEngine proof. */
void setEqualityEngineProof();
bool hasEqualityEngineProof() const;
@@ -662,7 +647,10 @@ class Constraint {
*/
ConstraintP getFloor();
- static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r);
+ static ConstraintP makeNegation(ArithVar v,
+ ConstraintType t,
+ const DeltaRational& r,
+ bool produceProofs);
const ValueCollection& getValueCollection() const;
@@ -799,12 +787,13 @@ class Constraint {
ConstraintP constraint = crp->d_constraint;
Assert(constraint->d_crid != ConstraintRuleIdSentinel);
constraint->d_crid = ConstraintRuleIdSentinel;
- ARITH_PROOF({
+ if (constraint->isProofProducing())
+ {
if (crp->d_farkasCoefficients != RationalVectorCPSentinel)
{
delete crp->d_farkasCoefficients;
}
- });
+ }
}
};
@@ -890,7 +879,7 @@ class Constraint {
inline RationalVectorCP getFarkasCoefficients() const
{
- return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients);
+ return d_produceProofs ? getConstraintRule().d_farkasCoefficients : nullptr;
}
void debugPrint() const;
@@ -993,6 +982,9 @@ class Constraint {
*/
SortedConstraintMapIterator d_variablePosition;
+ /** Whether to produce proofs, */
+ bool d_produceProofs;
+
}; /* class ConstraintValue */
std::ostream& operator<<(std::ostream& o, const Constraint& c);
@@ -1003,9 +995,9 @@ std::ostream& operator<<(std::ostream& o, const ValueCollection& c);
std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v);
std::ostream& operator<<(std::ostream& o, const ArithProofType);
-
-class ConstraintDatabase {
-private:
+class ConstraintDatabase : protected EnvObj
+{
+ private:
/**
* The map from ArithVars to their unique databases.
* When the vector changes size, we cannot allow the maps to move so this
@@ -1105,7 +1097,6 @@ private:
ArithCongruenceManager& d_congruenceManager;
- const context::Context * const d_satContext;
/** Owned by the TheoryArithPrivate, used here. */
EagerProofGenerator* d_pfGen;
/** Owned by the TheoryArithPrivate, used here. */
@@ -1120,13 +1111,11 @@ private:
friend class Constraint;
public:
- ConstraintDatabase(context::Context* satContext,
- context::Context* userContext,
+ ConstraintDatabase(Env& env,
const ArithVariables& variables,
ArithCongruenceManager& dm,
RaiseConflict conflictCallBack,
- EagerProofGenerator* pfGen,
- ProofNodeManager* pnm);
+ EagerProofGenerator* pfGen);
~ConstraintDatabase();
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 47dd208c1..8e7588847 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -482,7 +482,9 @@ const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool ro
return NULL;
}
-void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
+void LinearEqualityModule::propagateBasicFromRow(ConstraintP c,
+ bool produceProofs)
+{
Assert(c != NullConstraint);
Assert(c->isUpperBound() || c->isLowerBound());
Assert(!c->assertedToTheTheory());
@@ -493,7 +495,7 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
RowIndex ridx = d_tableau.basicToRowIndex(basic);
ConstraintCPVec bounds;
- RationalVectorP coeffs = ARITH_NULLPROOF(new RationalVector());
+ RationalVectorP coeffs = produceProofs ? new RationalVector() : nullptr;
propagateRow(bounds, ridx, upperBound, c, coeffs);
c->impliedByFarkas(bounds, coeffs, false);
c->tryToPropagate();
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 7195a6583..9a08530ec 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -417,87 +417,86 @@ public:
* The constraint on a basic variable b is implied by the constraints
* on its row. This is a wrapper for propagateRow().
*/
- void propagateBasicFromRow(ConstraintP c);
-
- /**
- * Let v be the variable for the constraint c.
- * Exports either the explanation of an upperbound or a lower bound
- * of v using the other variables in the row.
- *
- * If farkas != RationalVectorPSentinel, this function additionally
- * stores the farkas coefficients of the constraints stored in into.
- * Position 0 is the coefficient of v.
- * Position i > 0, corresponds to the order of the other constraints.
- */
- void propagateRow(ConstraintCPVec& into
- , RowIndex ridx
- , bool rowUp
- , ConstraintP c
- , RationalVectorP farkas);
-
- /**
- * Computes the value of a basic variable using the assignments
- * of the values of the variables in the basic variable's row tableau.
- * This can compute the value using either:
- * - the the current assignment (useSafe=false) or
- * - the safe assignment (useSafe = true).
- */
- DeltaRational computeRowValue(ArithVar x, bool useSafe) const;
-
- /**
- * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
- * and 2 ArithVar variables and returns one of the ArithVar variables
- * potentially using the internals of the SimplexDecisionProcedure.
- */
-
- ArithVar noPreference(ArithVar x, ArithVar y) const{
- return x;
- }
-
- /**
- * minVarOrder is a PreferenceFunction for selecting the smaller of the 2
- * ArithVars. This PreferenceFunction is used during the VarOrder stage of
- * findModel.
- */
- ArithVar minVarOrder(ArithVar x, ArithVar y) const;
-
- /**
- * minColLength is a PreferenceFunction for selecting the variable with the
- * smaller row count in the tableau.
- *
- * This is a heuristic rule and should not be used during the VarOrder
- * stage of findModel.
- */
- ArithVar minColLength(ArithVar x, ArithVar y) const;
-
- /**
- * minRowLength is a PreferenceFunction for selecting the variable with the
- * smaller row count in the tableau.
- *
- * This is a heuristic rule and should not be used during the VarOrder
- * stage of findModel.
- */
- ArithVar minRowLength(ArithVar x, ArithVar y) const;
-
- /**
- * minBoundAndRowCount is a PreferenceFunction for preferring a variable
- * without an asserted bound over variables with an asserted bound.
- * If both have bounds or both do not have bounds,
- * the rule falls back to minRowCount(...).
- *
- * This is a heuristic rule and should not be used during the VarOrder
- * stage of findModel.
- */
- ArithVar minBoundAndColLength(ArithVar x, ArithVar y) const;
-
-
- template <bool above>
- inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const {
- return
- ( above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic)) ||
- ( above && sgn > 0 && d_variables.strictlyAboveLowerBound(nonbasic)) ||
- (!above && sgn > 0 && d_variables.strictlyBelowUpperBound(nonbasic)) ||
- (!above && sgn < 0 && d_variables.strictlyAboveLowerBound(nonbasic));
+ void propagateBasicFromRow(ConstraintP c, bool produceProofs);
+
+ /**
+ * Let v be the variable for the constraint c.
+ * Exports either the explanation of an upperbound or a lower bound
+ * of v using the other variables in the row.
+ *
+ * If farkas != RationalVectorPSentinel, this function additionally
+ * stores the farkas coefficients of the constraints stored in into.
+ * Position 0 is the coefficient of v.
+ * Position i > 0, corresponds to the order of the other constraints.
+ */
+ void propagateRow(ConstraintCPVec& into,
+ RowIndex ridx,
+ bool rowUp,
+ ConstraintP c,
+ RationalVectorP farkas);
+
+ /**
+ * Computes the value of a basic variable using the assignments
+ * of the values of the variables in the basic variable's row tableau.
+ * This can compute the value using either:
+ * - the the current assignment (useSafe=false) or
+ * - the safe assignment (useSafe = true).
+ */
+ DeltaRational computeRowValue(ArithVar x, bool useSafe) const;
+
+ /**
+ * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
+ * and 2 ArithVar variables and returns one of the ArithVar variables
+ * potentially using the internals of the SimplexDecisionProcedure.
+ */
+
+ ArithVar noPreference(ArithVar x, ArithVar y) const { return x; }
+
+ /**
+ * minVarOrder is a PreferenceFunction for selecting the smaller of the 2
+ * ArithVars. This PreferenceFunction is used during the VarOrder stage of
+ * findModel.
+ */
+ ArithVar minVarOrder(ArithVar x, ArithVar y) const;
+
+ /**
+ * minColLength is a PreferenceFunction for selecting the variable with the
+ * smaller row count in the tableau.
+ *
+ * This is a heuristic rule and should not be used during the VarOrder
+ * stage of findModel.
+ */
+ ArithVar minColLength(ArithVar x, ArithVar y) const;
+
+ /**
+ * minRowLength is a PreferenceFunction for selecting the variable with the
+ * smaller row count in the tableau.
+ *
+ * This is a heuristic rule and should not be used during the VarOrder
+ * stage of findModel.
+ */
+ ArithVar minRowLength(ArithVar x, ArithVar y) const;
+
+ /**
+ * minBoundAndRowCount is a PreferenceFunction for preferring a variable
+ * without an asserted bound over variables with an asserted bound.
+ * If both have bounds or both do not have bounds,
+ * the rule falls back to minRowCount(...).
+ *
+ * This is a heuristic rule and should not be used during the VarOrder
+ * stage of findModel.
+ */
+ ArithVar minBoundAndColLength(ArithVar x, ArithVar y) const;
+
+ template <bool above>
+ inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const
+ {
+ return (above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic))
+ || (above && sgn > 0 && d_variables.strictlyAboveLowerBound(nonbasic))
+ || (!above && sgn > 0
+ && d_variables.strictlyBelowUpperBound(nonbasic))
+ || (!above && sgn < 0
+ && d_variables.strictlyAboveLowerBound(nonbasic));
}
/**
diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h
deleted file mode 100644
index c794c3b00..000000000
--- a/src/theory/arith/proof_macros.h
+++ /dev/null
@@ -1,32 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- * Alex Ozdemir, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Macros which run code when the old or new proof system is enabled,
- * or unsat cores are enabled.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H
-#define CVC5__THEORY__ARITH__PROOF_MACROS_H
-
-#include "options/smt_options.h"
-
-#define ARITH_PROOF(x) \
- if (cvc5::options::produceProofs()) \
- { \
- x; \
- }
-#define ARITH_NULLPROOF(x) (cvc5::options::produceProofs()) ? x : NULL
-#define ARITH_PROOF_ON() cvc5::options::produceProofs()
-
-#endif // CVC5__THEORY__ARITH__PROOF_MACROS_H
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 781f132d7..ed81f9e78 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -18,6 +18,7 @@
#include "base/output.h"
#include "options/arith_options.h"
+#include "options/smt_options.h"
#include "theory/arith/constraint.h"
#include "theory/arith/error_set.h"
#include "theory/arith/linear_equality.h"
@@ -49,7 +50,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
{
d_heuristicRule = options::arithErrorSelectionRule();
d_errorSet.setSelectionRule(d_heuristicRule);
- d_conflictBuilder = new FarkasConflictBuilder();
+ d_conflictBuilder = new FarkasConflictBuilder(options::produceProofs());
}
SimplexDecisionProcedure::~SimplexDecisionProcedure(){
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c0c51f7da..8e6bb6ccc 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -37,6 +37,7 @@
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "options/base_options.h"
+#include "options/smt_options.h"
#include "preprocessing/util/ite_utilities.h"
#include "proof/proof_generator.h"
#include "proof/proof_node_manager.h"
@@ -97,13 +98,11 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
: nullptr),
d_checker(),
d_pfGen(new EagerProofGenerator(d_pnm, userContext())),
- d_constraintDatabase(context(),
- userContext(),
+ d_constraintDatabase(d_env,
d_partialModel,
d_congruenceManager,
RaiseConflict(*this),
- d_pfGen.get(),
- d_pnm),
+ d_pfGen.get()),
d_qflraStatus(Result::SAT_UNKNOWN),
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
@@ -1749,7 +1748,7 @@ void TheoryArithPrivate::outputConflicts(){
const ConstraintRule& pf = confConstraint->getConstraintRule();
if (Debug.isOn("arith::conflict"))
{
- pf.print(std::cout);
+ pf.print(std::cout, options().smt.produceProofs);
std::cout << std::endl;
}
if (Debug.isOn("arith::pf::tree"))
@@ -4130,7 +4129,7 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
}
if(!assertedToTheTheory && canBePropagated && !hasProof ){
- d_linEq.propagateBasicFromRow(bestImplied);
+ d_linEq.propagateBasicFromRow(bestImplied, options().smt.produceProofs);
// I think this can be skipped if canBePropagated is true
//d_learnedBounds.push(bestImplied);
if(Debug.isOn("arith::prop")){
@@ -4435,8 +4434,12 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
if( !assertedToTheTheory && canBePropagated && !hasProof ){
ConstraintCPVec explain;
- ARITH_PROOF(d_farkasBuffer.clear());
- RationalVectorP coeffs = ARITH_NULLPROOF(&d_farkasBuffer);
+ if (options().smt.produceProofs)
+ {
+ d_farkasBuffer.clear();
+ }
+ RationalVectorP coeffs =
+ options().smt.produceProofs ? &d_farkasBuffer : nullptr;
// After invoking `propegateRow`:
// * coeffs[0] is for implied
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback