This decouples the arithmetic rewriter, the operator eliminator and the non-linear extension from TheoryArithPrivate and performs some minor cleanup.
This is in preparation for further refactoring of (lazy) arithmetic operator elimination.
theory/arith/theory_arith.h
theory/arith/theory_arith_private.cpp
theory/arith/theory_arith_private.h
- theory/arith/theory_arith_private_forward.h
theory/arith/theory_arith_type_rules.h
theory/arith/type_enumerator.h
theory/arrays/array_info.cpp
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
#include "theory/arith/constraint_forward.h"
-#include "theory/arith/theory_arith_private_forward.h"
#include "util/rational.h"
namespace CVC4 {
namespace theory {
namespace arith {
+class TheoryArithPrivate;
+
/**
* ArithVarCallBack provides a mechanism for agreeing on callbacks while
* breaking mutual recursion inclusion order problems.
namespace CVC4 {
namespace theory {
-
-namespace quantifiers {
-class EqualityInference;
-}
-
namespace arith {
class ArithCongruenceManager {
d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
d_astate(*d_internal, c, u, valuation),
d_inferenceManager(*this, d_astate, pnm),
- d_nonlinearExtension(nullptr)
+ d_nonlinearExtension(nullptr),
+ d_opElim(pnm, logicInfo)
{
smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
delete d_internal;
}
-TheoryRewriter* TheoryArith::getTheoryRewriter()
-{
- return d_internal->getTheoryRewriter();
-}
+TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
{
TrustNode TheoryArith::expandDefinition(Node node)
{
- return d_internal->expandDefinition(node);
+ // call eliminate operators
+ return d_opElim.eliminate(node);
}
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
TrustNode TheoryArith::ppRewrite(TNode atom)
{
CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
- return d_internal->ppRewrite(atom);
+ Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
+
+ if (options::arithRewriteEq())
+ {
+ if (atom.getKind() == kind::EQUAL && atom[0].getType().isReal())
+ {
+ Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+ Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+ TrustNode tleq = ppRewriteTerms(leq);
+ TrustNode tgeq = ppRewriteTerms(geq);
+ if (!tleq.isNull())
+ {
+ leq = tleq.getNode();
+ }
+ if (!tgeq.isNull())
+ {
+ geq = tgeq.getNode();
+ }
+ Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+ Debug("arith::preprocess")
+ << "arith::preprocess() : returning " << rewritten << endl;
+ // don't need to rewrite terms since rewritten is not a non-standard op
+ return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
+ }
+ }
+ return ppRewriteTerms(atom);
+}
+
+TrustNode TheoryArith::ppRewriteTerms(TNode n)
+{
+ if (Theory::theoryOf(n) != THEORY_ARITH)
+ {
+ return TrustNode::null();
+ }
+ // Eliminate operators recursively. Notice we must do this here since other
+ // theories may generate lemmas that involve non-standard operators. For
+ // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
+ // introduce non-standard arithmetic terms appearing in grammars.
+ // call eliminate operators
+ return d_opElim.eliminate(n);
}
Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
return;
}
// otherwise, check with the linear solver
- d_internal->postCheck(level);
+ if (d_internal->postCheck(level))
+ {
+ // linear solver emitted a conflict or lemma, return
+ return;
+ }
+
+ if (Theory::fullEffort(level))
+ {
+ if (d_nonlinearExtension != nullptr)
+ {
+ d_nonlinearExtension->check(level);
+ }
+ else if (d_internal->foundNonlinear())
+ {
+ // set incomplete
+ d_inferenceManager.setIncomplete();
+ }
+ }
}
bool TheoryArith::preNotifyFact(
#pragma once
#include "expr/node.h"
+#include "theory/arith/arith_rewriter.h"
#include "theory/arith/arith_state.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/nonlinear_extension.h"
-#include "theory/arith/theory_arith_private_forward.h"
+#include "theory/arith/operator_elim.h"
#include "theory/theory.h"
namespace CVC4 {
namespace theory {
namespace arith {
+class TheoryArithPrivate;
+
/**
* Implementation of linear and non-linear integer and real arithmetic.
* The linear arithmetic solver is based upon:
}
private:
+ /**
+ * Preprocess rewrite terms, return the trust node encapsulating the
+ * preprocessed form of n, and the proof generator that can provide the
+ * proof for the equivalence of n and this term.
+ *
+ * This calls the operator elimination utility to eliminate extended
+ * symbols.
+ */
+ TrustNode ppRewriteTerms(TNode n);
/** Get the proof equality engine */
eq::ProofEqEngine* getProofEqEngine();
/** The state object wrapping TheoryArithPrivate */
* arithmetic.
*/
std::unique_ptr<nl::NonlinearExtension> d_nonlinearExtension;
+ /** The operator elimination utility */
+ OperatorElim d_opElim;
+ /** The theory rewriter for this theory. */
+ ArithRewriter d_rewriter;
};/* class TheoryArith */
}/* CVC4::theory::arith namespace */
const LogicInfo& logicInfo,
ProofNodeManager* pnm)
: d_containing(containing),
- d_nlIncomplete(false),
+ d_foundNl(false),
d_rowTracking(),
d_pnm(pnm),
d_checker(),
d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_attemptSolSimplex(
d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
- d_nonlinearExtension(nullptr),
d_pass1SDP(NULL),
d_otherSDP(NULL),
d_lastContextIntegerAttempted(c, -1),
d_solveIntAttempts(0u),
d_newFacts(false),
d_previousStatus(Result::SAT_UNKNOWN),
- d_statistics(),
- d_opElim(pnm, logicInfo)
+ d_statistics()
{
ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
if (pc != nullptr)
if(d_approxStats != NULL) { delete d_approxStats; }
}
-TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; }
bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
{
return d_congruenceManager.needsEqualityEngine(esi);
eq::ProofEqEngine* pfee = d_containing.getProofEqEngine();
Assert(ee != nullptr);
d_congruenceManager.finishInit(ee, pfee);
- d_nonlinearExtension = d_containing.d_nonlinearExtension.get();
}
static bool contains(const ConstraintCPVec& v, ConstraintP con){
}
}
-TrustNode TheoryArithPrivate::ppRewriteTerms(TNode n)
-{
- if(Theory::theoryOf(n) != THEORY_ARITH) {
- return TrustNode::null();
- }
- // Eliminate operators recursively. Notice we must do this here since other
- // theories may generate lemmas that involve non-standard operators. For
- // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
- // introduce non-standard arithmetic terms appearing in grammars.
- // call eliminate operators
- return d_opElim.eliminate(n);
-}
-
-TrustNode TheoryArithPrivate::ppRewrite(TNode atom)
-{
- Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
-
- if (options::arithRewriteEq())
- {
- if (atom.getKind() == kind::EQUAL && atom[0].getType().isReal())
- {
- Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
- Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
- TrustNode tleq = ppRewriteTerms(leq);
- TrustNode tgeq = ppRewriteTerms(geq);
- if (!tleq.isNull())
- {
- leq = tleq.getNode();
- }
- if (!tgeq.isNull())
- {
- geq = tgeq.getNode();
- }
- Node rewritten = Rewriter::rewrite(leq.andNode(geq));
- Debug("arith::preprocess")
- << "arith::preprocess() : returning " << rewritten << endl;
- // don't need to rewrite terms since rewritten is not a non-standard op
- return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
- }
- }
- return ppRewriteTerms(atom);
-}
-
Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
Debug("simplify") << "TheoryArithPrivate::solve(" << in << ")" << endl;
if(getLogicInfo().isLinear()){
throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
}
-
- if (d_nonlinearExtension == nullptr)
- {
- d_nlIncomplete = true;
- }
+ d_foundNl = true;
++(d_statistics.d_statUserVariables);
requestArithVar(vlNode, false, false);
//setupInitialValue(av);
markSetup(vlNode);
- }else{
- if (d_nonlinearExtension == nullptr)
- {
- if (vlNode.getKind() == kind::EXPONENTIAL
- || vlNode.getKind() == kind::SINE || vlNode.getKind() == kind::COSINE
- || vlNode.getKind() == kind::TANGENT)
- {
- d_nlIncomplete = true;
- }
- }
+ }
+ else if (vlNode.getKind() == kind::EXPONENTIAL
+ || vlNode.getKind() == kind::SINE || vlNode.getKind() == kind::COSINE
+ || vlNode.getKind() == kind::TANGENT)
+ {
+ d_foundNl = true;
}
/* Note:
}
}
-void TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
+bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
{
if(!anyConflict()){
while(!d_learnedBounds.empty()){
}
outputConflicts();
//cout << "unate conflict 1 " << effortLevel << std::endl;
- return;
+ return true;
}
revertOutOfConflict();
d_errorSet.clear();
outputConflicts();
- return;
+ return true;
}
}
}
}//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
- if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){
- if (d_nonlinearExtension != nullptr)
- {
- d_nonlinearExtension->check( effortLevel );
- }
- }
-
- if(Theory::fullEffort(effortLevel) && d_nlIncomplete){
- setIncomplete();
- }
-
if(Theory::fullEffort(effortLevel)){
if(Debug.isOn("arith::consistency::final")){
entireStateIsConsistent("arith::consistency::final");
}
- // cout << "fulleffort" << getSatContext()->getLevel() << endl;
- // entireStateIsConsistent("arith::consistency::final");
- // cout << "emmittedConflictOrSplit" << emmittedConflictOrSplit << endl;
}
if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
debugPrintModel(Debug("arith::print_model"));
}
Debug("arith") << "TheoryArithPrivate::check end" << std::endl;
+ return emmittedConflictOrSplit;
}
+bool TheoryArithPrivate::foundNonlinear() const { return d_foundNl; }
+
Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
const DeltaRational& d = d_partialModel.getAssignment(x);
Assert(!d.isIntegral());
std::map<Node, Node>& arithModel)
{
AlwaysAssert(d_qflraStatus == Result::SAT);
- //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
if(Debug.isOn("arith::collectModelInfo")){
debugPrintFacts();
return d_rowTracking[ridx];
}
-TrustNode TheoryArithPrivate::expandDefinition(Node node)
-{
- // call eliminate operators
- return d_opElim.eliminate(node);
-}
-
std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
using namespace inferbounds;
#include "options/arith_options.h"
#include "smt/logic_exception.h"
#include "smt_util/boolean_simplification.h"
-#include "theory/arith/arith_rewriter.h"
#include "theory/arith/arith_static_learner.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/linear_equality.h"
#include "theory/arith/matrix.h"
#include "theory/arith/normal_form.h"
-#include "theory/arith/operator_elim.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/proof_checker.h"
#include "theory/arith/simplex.h"
#include "theory/arith/soi_simplex.h"
#include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private_forward.h"
#include "theory/eager_proof_generator.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
}
class InferBoundsResult;
-namespace nl {
-class NonlinearExtension;
-}
-
/**
* Implementation of QF_LRA.
* Based upon:
TheoryArith& d_containing;
- bool d_nlIncomplete;
- // TODO A better would be:
- //context::CDO<bool> d_nlIncomplete;
+ /**
+ * Whether we encountered non-linear arithmetic at any time during solving.
+ */
+ bool d_foundNl;
BoundInfoMap d_rowTracking;
SumOfInfeasibilitiesSPD d_soiSimplex;
AttemptSolutionSDP d_attemptSolSimplex;
- /** non-linear algebraic approach */
- nl::NonlinearExtension* d_nonlinearExtension;
-
bool solveRealRelaxation(Theory::Effort effortLevel);
/* Returns true if this is heuristically a good time to try
Node axiomIteForTotalDivision(Node div_tot);
Node axiomIteForTotalIntDivision(Node int_div_like);
-
- // handle linear /, div, mod, and also is_int, to_int
- TrustNode ppRewriteTerms(TNode atom);
-
public:
TheoryArithPrivate(TheoryArith& containing,
context::Context* c,
~TheoryArithPrivate();
//--------------------------------- initialization
- /** get the official theory rewriter of this theory */
- TheoryRewriter* getTheoryRewriter();
/**
* Returns true if we need an equality engine, see
* Theory::needsEqualityEngine.
* Does non-context dependent setup for a node connected to a theory.
*/
void preRegisterTerm(TNode n);
- TrustNode expandDefinition(Node node);
void propagate(Theory::Effort e);
Node explain(TNode n);
void presolve();
void notifyRestart();
Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
- TrustNode ppRewrite(TNode atom);
void ppStaticLearn(TNode in, NodeBuilder<>& learned);
std::string identify() const { return std::string("TheoryArith"); }
bool preCheck(Theory::Effort level);
/** Pre-notify fact. */
void preNotifyFact(TNode atom, bool pol, TNode fact);
- /** Post-check, called after the fact queue of the theory is processed. */
- void postCheck(Theory::Effort level);
+ /**
+ * Post-check, called after the fact queue of the theory is processed. Returns
+ * true if a conflict or lemma was emitted.
+ */
+ bool postCheck(Theory::Effort level);
//--------------------------------- end standard check
+ /**
+ * Found non-linear? This returns true if this solver ever encountered
+ * any non-linear terms that were unhandled. Note that this class is not
+ * responsible for handling non-linear arithmetic. If the owner of this
+ * class does not handle non-linear arithmetic in another way, then
+ * setIncomplete should be called on the output channel of TheoryArith.
+ */
+ bool foundNonlinear() const;
+
private:
/** The constant zero. */
DeltaRational d_DELTA_ZERO;
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(); }
- inline void setIncomplete() {
- (d_containing.d_out)->setIncomplete();
- d_nlIncomplete = true;
- }
void outputLemma(TNode lem);
void outputConflict(TNode lit);
void outputPropagate(TNode lit);
Statistics d_statistics;
-
- /** The theory rewriter for this theory. */
- ArithRewriter d_rewriter;
- /** The operator elimination utility */
- OperatorElim d_opElim;
};/* class TheoryArithPrivate */
}/* CVC4::theory::arith namespace */
+++ /dev/null
-/********************* */
-/*! \file theory_arith_private_forward.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "cvc4_private.h"
-
-#pragma once
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class TheoryArithPrivate;
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
projects / cvc5.git / commitdiff