This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.
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
#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 {
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();
}
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){
} 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);
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;
}
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();
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
#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"
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){
}
}
-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());
}
{
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;
}
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() << " [";
}
}
-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;
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; }
&& 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:
{
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:
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)
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){
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;
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;
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);
}
if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
- getConstraintRule().print(Debug("constraints::wffp"));
+ getConstraintRule().print(Debug("constraints::wffp"), d_produceProofs);
}
Assert(wellFormedFarkasProof());
}
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);
AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
RationalVectorCP coeffsCopy;
- if (ARITH_PROOF_ON())
+ if (d_produceProofs)
{
Assert(coeffs != RationalVectorCPSentinel);
coeffsCopy = new RationalVector(*coeffs);
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());
}
{
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());
#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 {
* 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 */
* 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.
/** 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;
*/
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;
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;
}
- });
+ }
}
};
inline RationalVectorCP getFarkasCoefficients() const
{
- return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients);
+ return d_produceProofs ? getConstraintRule().d_farkasCoefficients : nullptr;
}
void debugPrint() const;
*/
SortedConstraintMapIterator d_variablePosition;
+ /** Whether to produce proofs, */
+ bool d_produceProofs;
+
}; /* class ConstraintValue */
std::ostream& operator<<(std::ostream& o, const Constraint& 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
ArithCongruenceManager& d_congruenceManager;
- const context::Context * const d_satContext;
/** Owned by the TheoryArithPrivate, used here. */
EagerProofGenerator* d_pfGen;
/** Owned by the TheoryArithPrivate, used here. */
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();
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());
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();
* 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));
}
/**
+++ /dev/null
-/******************************************************************************
- * 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
#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"
{
d_heuristicRule = options::arithErrorSelectionRule();
d_errorSet.setSelectionRule(d_heuristicRule);
- d_conflictBuilder = new FarkasConflictBuilder();
+ d_conflictBuilder = new FarkasConflictBuilder(options::produceProofs());
}
SimplexDecisionProcedure::~SimplexDecisionProcedure(){
#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"
: 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),
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"))
}
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")){
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
projects / cvc5.git / commitdiff