From 3051fd4ea618348da9a0b856b7bb07fcda027839 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Oct 2020 09:06:02 -0500 Subject: [PATCH] Decouple modules from TheoryArithPrivate (#5184) 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. --- src/CMakeLists.txt | 1 - src/theory/arith/callbacks.h | 3 +- src/theory/arith/congruence_manager.h | 5 - src/theory/arith/theory_arith.cpp | 71 ++++++++++-- src/theory/arith/theory_arith.h | 18 ++- src/theory/arith/theory_arith_private.cpp | 103 +++--------------- src/theory/arith/theory_arith_private.h | 50 +++------ .../arith/theory_arith_private_forward.h | 31 ------ 8 files changed, 115 insertions(+), 167 deletions(-) delete mode 100644 src/theory/arith/theory_arith_private_forward.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7c22b880a..3ca20e8dc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -395,7 +395,6 @@ libcvc4_add_sources( 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 diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index d9d9708a8..1ce61f46f 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -22,13 +22,14 @@ #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. diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 67df9237c..6115fec8a 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -38,11 +38,6 @@ namespace CVC4 { namespace theory { - -namespace quantifiers { -class EqualityInference; -} - namespace arith { class ArithCongruenceManager { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 93c8d87fc..434d2e1c8 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -44,7 +44,8 @@ TheoryArith::TheoryArith(context::Context* c, 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); @@ -58,10 +59,7 @@ TheoryArith::~TheoryArith(){ delete d_internal; } -TheoryRewriter* TheoryArith::getTheoryRewriter() -{ - return d_internal->getTheoryRewriter(); -} +TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; } bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi) { @@ -101,7 +99,8 @@ void TheoryArith::preRegisterTerm(TNode n) 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); } @@ -109,7 +108,46 @@ 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) { @@ -134,7 +172,24 @@ void TheoryArith::postCheck(Effort level) 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( diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index f05dee38b..8555156a5 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -18,16 +18,19 @@ #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: @@ -120,6 +123,15 @@ class TheoryArith : public Theory { } 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 */ @@ -132,6 +144,10 @@ class TheoryArith : public Theory { * arithmetic. */ std::unique_ptr d_nonlinearExtension; + /** The operator elimination utility */ + OperatorElim d_opElim; + /** The theory rewriter for this theory. */ + ArithRewriter d_rewriter; };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 1a13f44fa..557072319 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -92,7 +92,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, const LogicInfo& logicInfo, ProofNodeManager* pnm) : d_containing(containing), - d_nlIncomplete(false), + d_foundNl(false), d_rowTracking(), d_pnm(pnm), d_checker(), @@ -147,7 +147,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, 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), @@ -171,8 +170,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, 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) @@ -186,7 +184,6 @@ TheoryArithPrivate::~TheoryArithPrivate(){ if(d_approxStats != NULL) { delete d_approxStats; } } -TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; } bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi) { return d_congruenceManager.needsEqualityEngine(esi); @@ -197,7 +194,6 @@ void TheoryArithPrivate::finishInit() 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){ @@ -1107,49 +1103,6 @@ Node TheoryArithPrivate::getModelValue(TNode term) { } } -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; @@ -1296,11 +1249,7 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ 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); @@ -1308,16 +1257,12 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ //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: @@ -3332,7 +3277,7 @@ void TheoryArithPrivate::preNotifyFact(TNode atom, bool pol, TNode fact) } } -void TheoryArithPrivate::postCheck(Theory::Effort effortLevel) +bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) { if(!anyConflict()){ while(!d_learnedBounds.empty()){ @@ -3368,7 +3313,7 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } outputConflicts(); //cout << "unate conflict 1 " << effortLevel << std::endl; - return; + return true; } @@ -3403,7 +3348,7 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel) revertOutOfConflict(); d_errorSet.clear(); outputConflicts(); - return; + return true; } } @@ -3641,24 +3586,10 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } }//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(); } @@ -3666,8 +3597,11 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel) 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()); @@ -4075,7 +4009,6 @@ void TheoryArithPrivate::collectModelValues(const std::set& termSet, std::map& 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(); @@ -4687,12 +4620,6 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ return d_rowTracking[ridx]; } -TrustNode TheoryArithPrivate::expandDefinition(Node node) -{ - // call eliminate operators - return d_opElim.eliminate(node); -} - std::pair TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ using namespace inferbounds; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 71bada17d..1d840a81f 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -35,7 +35,6 @@ #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" @@ -50,13 +49,11 @@ #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" @@ -82,10 +79,6 @@ namespace inferbounds { } class InferBoundsResult; -namespace nl { -class NonlinearExtension; -} - /** * Implementation of QF_LRA. * Based upon: @@ -98,9 +91,10 @@ private: TheoryArith& d_containing; - bool d_nlIncomplete; - // TODO A better would be: - //context::CDO d_nlIncomplete; + /** + * Whether we encountered non-linear arithmetic at any time during solving. + */ + bool d_foundNl; BoundInfoMap d_rowTracking; @@ -382,9 +376,6 @@ private: 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 @@ -426,10 +417,6 @@ private: 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, @@ -441,8 +428,6 @@ private: ~TheoryArithPrivate(); //--------------------------------- initialization - /** get the official theory rewriter of this theory */ - TheoryRewriter* getTheoryRewriter(); /** * Returns true if we need an equality engine, see * Theory::needsEqualityEngine. @@ -456,7 +441,6 @@ private: * 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); @@ -482,7 +466,6 @@ private: 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"); } @@ -502,9 +485,21 @@ private: 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; @@ -692,10 +687,6 @@ private: 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); @@ -877,11 +868,6 @@ private: 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 */ diff --git a/src/theory/arith/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h deleted file mode 100644 index 6668e0386..000000000 --- a/src/theory/arith/theory_arith_private_forward.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* */ -/*! \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 */ -- 2.30.2