diff options
35 files changed, 3224 insertions, 221 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 5caed7b14..e44bd920c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -220,6 +220,8 @@ libcvc4_la_SOURCES = \ theory/arith/linear_equality.h \ theory/arith/matrix.cpp \ theory/arith/matrix.h \ + theory/arith/nonlinear_extension.h \ + theory/arith/nonlinear_extension.cpp \ theory/arith/normal_form.cpp \ theory/arith/normal_form.h\ theory/arith/partial_model.cpp \ diff --git a/src/options/arith_options b/src/options/arith_options index f38e377ba..6f76758e3 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -165,4 +165,28 @@ option pbRewriteThreshold --pb-rewrite-threshold int :default 256 option sNormInferEq --snorm-infer-eq bool :default false infer equalities based on Shostak normalization +option nlAlg --nl-alg bool :default false + algebraic approach to non-linear + +option nlAlgResBound --nl-alg-rbound bool :default false + use resolution-style inference for inferring new bounds + +option nlAlgTangentPlanes --nl-alg-tplanes bool :default false + use non-terminating tangent plane strategy for non-linear + +option nlAlgEntailConflicts --nl-alg-ent-conf bool :default false + check for entailed conflicts in non-linear solver + +option nlAlgRewrites --nl-alg-rewrite bool :default true + do rewrites in non-linear solver + +option nlAlgSolveSubs --nl-alg-solve-subs bool :default true + do solving for determining constant substitutions + +option nlAlgPurify --nl-alg-purify bool :default false + purify non-linear terms at preprocess + +option nlAlgSplitZero --nl-alg-split-zero bool :default false + intial splits on zero for all variables + endmodule diff --git a/src/options/smt_options b/src/options/smt_options index 747119344..8f681e57d 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -162,4 +162,7 @@ option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default fa undocumented-option solveIntAsBV --solve-int-as-bv uint32_t :default 0 attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental) +undocumented-option solveRealAsInt --solve-real-as-int bool :default false + attempt to solve a pure real satisfiable problem as a integer problem (for non-linear) + endmodule diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index c9a80d247..7b0ccdb8a 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -497,6 +497,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo opType = INFIX; break; case kind::MULT: + case kind::NONLINEAR_MULT: op << '*'; opType = INFIX; break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 08eaf610a..fcb6be366 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -369,6 +369,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // arith theory case kind::PLUS: case kind::MULT: + case kind::NONLINEAR_MULT: case kind::MINUS: case kind::UMINUS: case kind::LT: @@ -738,7 +739,8 @@ static string smtKindString(Kind k) throw() { // arith theory case kind::PLUS: return "+"; - case kind::MULT: return "*"; + case kind::MULT: + case kind::NONLINEAR_MULT: return "*"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; case kind::LT: return "<"; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 20cd5e83e..5ef77f9d8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -584,8 +584,10 @@ private: */ void removeITEs(); + Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq); Node intToBV(TNode n, NodeToNodeHashMap& cache); Node intToBVMakeBinary(TNode n, NodeToNodeHashMap& cache); + Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false); /** * Helper function to fix up assertion list to restore invariants needed after @@ -1272,9 +1274,10 @@ void SmtEngine::setLogicInternal() throw() { void SmtEngine::setDefaults() { if(options::forceLogicString.wasSetByUser()) { d_logic = LogicInfo(options::forceLogicString()); - } - else if (options::solveIntAsBV() > 0) { + }else if (options::solveIntAsBV() > 0) { d_logic = LogicInfo("QF_BV"); + }else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) { + d_logic = LogicInfo("QF_NIA"); } else if ((d_logic.getLogicString() == "QF_UFBV" || d_logic.getLogicString() == "QF_ABV") && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { @@ -1604,7 +1607,7 @@ void SmtEngine::setDefaults() { // Turn on arith rewrite equalities only for pure arithmetic if(! options::arithRewriteEq.wasSetByUser()) { - bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified(); + bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isQuantified(); Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << endl; options::arithRewriteEq.set(arithRewriteEq); } @@ -1976,9 +1979,8 @@ void SmtEngine::setDefaults() { options::arraysLazyRIntro1.set(false); } - // Non-linear arithmetic does not support models - if (d_logic.isTheoryEnabled(THEORY_ARITH) && - !d_logic.isLinear()) { + // Non-linear arithmetic does not support models unless nlAlg is enabled + if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlAlg() ) { if (options::produceModels()) { if(options::produceModels.wasSetByUser()) { throw OptionException("produce-model not supported with nonlinear arith"); @@ -2660,6 +2662,135 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) { return cache[n_binary]; } +Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& var_eq) { + Trace("real-as-int-debug") << "Convert : " << n << std::endl; + NodeMap::iterator find = cache.find(n); + if (find != cache.end()) { + return (*find).second; + }else{ + Node ret = n; + if( n.getNumChildren()>0 ){ + if( n.getKind()==kind::EQUAL || n.getKind()==kind::GEQ || n.getKind()==kind::LT || n.getKind()==kind::GT || n.getKind()==kind::LEQ ){ + ret = Rewriter::rewrite( n ); + Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl; + if( !ret.isConst() ){ + Node ret_lit = ret.getKind()==kind::NOT ? ret[0] : ret; + bool ret_pol = ret.getKind()!=kind::NOT; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( ret_lit, msum ) ){ + //get common coefficient + std::vector< Node > coeffs; + for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ + Node v = itm->first; + Node c = itm->second; + if( !c.isNull() ){ + Assert( c.isConst() ); + coeffs.push_back( NodeManager::currentNM()->mkConst( Rational( c.getConst<Rational>().getDenominator() ) ) ); + } + } + Node cc = coeffs.empty() ? Node::null() : ( coeffs.size()==1 ? coeffs[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, coeffs ) ) ); + std::vector< Node > sum; + for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ + Node v = itm->first; + Node c = itm->second; + Node s; + if( c.isNull() ){ + c = cc.isNull() ? NodeManager::currentNM()->mkConst( Rational( 1 ) ) : cc; + }else{ + if( !cc.isNull() ){ + c = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, c, cc ) ); + } + } + Assert( c.getType().isInteger() ); + if( v.isNull() ){ + sum.push_back( c ); + }else{ + Node vv = realToInt( v, cache, var_eq ); + if( vv.getType().isInteger() ){ + sum.push_back( NodeManager::currentNM()->mkNode( kind::MULT, c, vv ) ); + }else{ + throw TypeCheckingException(v.toExpr(), string("Cannot translate to Int: ") + v.toString()); + } + } + } + Node sumt = sum.empty() ? NodeManager::currentNM()->mkConst( Rational( 0 ) ) : ( sum.size()==1 ? sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, sum ) ); + ret = NodeManager::currentNM()->mkNode( ret_lit.getKind(), sumt, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + if( !ret_pol ){ + ret = ret.negate(); + } + Trace("real-as-int") << "Convert : " << std::endl; + Trace("real-as-int") << " " << n << std::endl; + Trace("real-as-int") << " " << ret << std::endl; + }else{ + throw TypeCheckingException(n.toExpr(), string("Cannot translate to Int: ") + n.toString()); + } + } + }else{ + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = realToInt( n[i], cache, var_eq ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + }else{ + if( n.isVar() ){ + if( !n.getType().isInteger() ){ + ret = NodeManager::currentNM()->mkSkolem("__realToInt_var", NodeManager::currentNM()->integerType(), "Variable introduced in realToInt pass"); + var_eq.push_back( n.eqNode( ret ) ); + } + } + } + cache[n] = ret; + return ret; + } +} + +Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) { + if( beneathMult ){ + NodeMap::iterator find = bcache.find(n); + if (find != bcache.end()) { + return (*find).second; + } + }else{ + NodeMap::iterator find = cache.find(n); + if (find != cache.end()) { + return (*find).second; + } + } + Node ret = n; + if( n.getNumChildren()>0 ){ + if( beneathMult && n.getKind()!=kind::MULT ){ + //new variable + ret = NodeManager::currentNM()->mkSkolem("__purifyNl_var", n.getType(), "Variable introduced in purifyNl pass"); + Node np = purifyNlTerms( n, cache, bcache, var_eq, false ); + var_eq.push_back( np.eqNode( ret ) ); + }else{ + bool beneathMultNew = beneathMult || n.getKind()==kind::MULT; + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + } + if( beneathMult ){ + bcache[n] = ret; + }else{ + cache[n] = ret; + } + return ret; +} + void SmtEnginePrivate::removeITEs() { d_smt.finalOptionsAreSet(); spendResource(options::preprocessStep()); @@ -3866,6 +3997,20 @@ void SmtEnginePrivate::processAssertions() { ); Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + + if( options::nlAlgPurify() ){ + hash_map<Node, Node, NodeHashFunction> cache; + hash_map<Node, Node, NodeHashFunction> bcache; + std::vector< Node > var_eq; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq)); + } + if( !var_eq.empty() ){ + unsigned lastIndex = d_assertions.size()-1; + var_eq.insert( var_eq.begin(), d_assertions[lastIndex] ); + d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) ); + } + } if( options::ceGuidedInst() ){ //register sygus conjecture pre-rewrite (motivated by solution reconstruction) @@ -3873,7 +4018,23 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] ); } } - + + if (options::solveRealAsInt()) { + Chat() << "converting reals to ints..." << endl; + hash_map<Node, Node, NodeHashFunction> cache; + std::vector< Node > var_eq; + for(unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq)); + } + /* + if( !var_eq.empty() ){ + unsigned lastIndex = d_assertions.size()-1; + var_eq.insert( var_eq.begin(), d_assertions[lastIndex] ); + d_assertions.replace(last_index, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) ); + } + */ + } + if (options::solveIntAsBV() > 0) { Chat() << "converting ints to bit-vectors..." << endl; hash_map<Node, Node, NodeHashFunction> cache; @@ -4361,7 +4522,7 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult(); - if (options::solveIntAsBV() > 0 &&r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) { r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 642216b40..6087ab70f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -100,6 +100,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::PLUS: return preRewritePlus(t); case kind::MULT: + case kind::NONLINEAR_MULT: return preRewriteMult(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: @@ -148,6 +149,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::PLUS: return postRewritePlus(t); case kind::MULT: + case kind::NONLINEAR_MULT: return postRewriteMult(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: @@ -222,7 +224,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ RewriteResponse ArithRewriter::preRewriteMult(TNode t){ - Assert(t.getKind()== kind::MULT); + Assert(t.getKind()== kind::MULT || t.getKind()== kind::NONLINEAR_MULT); if(t.getNumChildren() == 2){ if(t[0].getKind() == kind::CONST_RATIONAL @@ -316,7 +318,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t){ } RewriteResponse ArithRewriter::postRewriteMult(TNode t){ - Assert(t.getKind()== kind::MULT); + Assert(t.getKind()== kind::MULT || t.getKind()==kind::NONLINEAR_MULT); Polynomial res = Polynomial::mkOne(); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 14329ce4d..ba1a9b037 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -252,25 +252,65 @@ inline Node flattenAnd(Node n){ return NodeManager::currentNM()->mkNode(kind::AND, out); } +// Returns an node that is the identity of a select few kinds. inline Node getIdentity(Kind k){ switch(k){ case kind::AND: - return NodeManager::currentNM()->mkConst<bool>(true); + return mkBoolNode(true); case kind::PLUS: - return NodeManager::currentNM()->mkConst(Rational(1)); + return mkRationalNode(0); + case kind::MULT: + case kind::NONLINEAR_MULT: + return mkRationalNode(1); default: Unreachable(); } } -inline Node safeConstructNary(NodeBuilder<>& nb){ - switch(nb.getNumChildren()){ - case 0: return getIdentity(nb.getKind()); - case 1: return nb[0]; - default: return (Node)nb; +inline Node safeConstructNary(NodeBuilder<>& nb) { + switch (nb.getNumChildren()) { + case 0: + return getIdentity(nb.getKind()); + case 1: + return nb[0]; + default: + return (Node)nb; } } +inline Node safeConstructNary(Kind k, const std::vector<Node>& children) { + switch (children.size()) { + case 0: + return getIdentity(k); + case 1: + return children[0]; + default: + return NodeManager::currentNM()->mkNode(k, children); + } +} + +// Returns the multiplication of a and b. +inline Node mkMult(Node a, Node b) { + return NodeManager::currentNM()->mkNode(kind::MULT, a, b); +} + +// Return a constraint that is equivalent to term being is in the range +// [start, end). This includes start and excludes end. +inline Node mkInRange(Node term, Node start, Node end) { + NodeManager* nm = NodeManager::currentNM(); + Node above_start = nm->mkNode(kind::LEQ, start, term); + Node below_end = nm->mkNode(kind::LT, term, end); + return nm->mkNode(kind::AND, above_start, below_end); +} + +// Creates an expression that constrains q to be equal to one of two expressions +// when n is 0 or not. Useful for division by 0 logic. +// (ite (= n 0) (= q if_zero) (= q not_zero)) +inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero) { + Node zero = mkRationalNode(0); + return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero)); +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index da69436f1..25822afdf 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -42,6 +42,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_avariables(avars), d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) { + d_ee.addFunctionKind(kind::NONLINEAR_MULT); //module to infer additional equalities based on normalization if( options::sNormInferEq() ){ d_eq_infer = new quantifiers::EqualityInference(c, true); @@ -513,8 +514,6 @@ bool ArithCongruenceManager::fixpointInfer() { return inConflict(); } - - }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index a02f36a0f..8d92a4153 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -175,6 +175,9 @@ public: /** process inferred equalities based on Shostak normalization */ bool fixpointInfer(); + + eq::EqualityEngine * getEqualityEngine() { return &d_ee; } + private: class Statistics { public: diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 45470180b..61029ac48 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -14,6 +14,7 @@ rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" operator PLUS 2: "arithmetic addition (N-ary)" operator MULT 2: "arithmetic multiplication (N-ary)" +operator NONLINEAR_MULT 2: "synonym for MULT" operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "real division, division by 0 undefined (user symbol)" @@ -85,6 +86,7 @@ operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule +typerule NONLINEAR_MULT ::CVC4::theory::arith::ArithOperatorTypeRule typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp new file mode 100644 index 000000000..366bff4eb --- /dev/null +++ b/src/theory/arith/nonlinear_extension.cpp @@ -0,0 +1,2182 @@ +/********************* */ +/*! \file nl_alg.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 "theory/arith/nonlinear_extension.h" + +#include <set> + +#include "expr/node_builder.h" +#include "options/arith_options.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/theory_arith.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/theory_model.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { + +namespace { + +// Return true if a collection c contains an elem k. Compatible with map and set +// containers. +template <class Container, class Key> +bool Contains(const Container& c, const Key& k) { + return c.find(k) != c.end(); +} + +// Inserts value into the set/map c if the value was not present there. Returns +// true if the value was inserted. +template <class Container, class Value> +bool InsertIfNotPresent(Container* c, const Value& value) { + return (c->insert(value)).second; +} + +// Returns true if a vector c contains an elem t. +template <class T> +bool IsInVector(const std::vector<T>& c, const T& t) { + return std::find(c.begin(), c.end(), t) != c.end(); +} + +// Returns the a[key] and assertion fails in debug mode. +inline unsigned getCount(const NodeMultiset& a, Node key) { + NodeMultiset::const_iterator it = a.find(key); + Assert(it != a.end()); + return it->second; +} + +// Returns a[key] if key is in a or value otherwise. +unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value) { + NodeMultiset::const_iterator it = a.find(key); + return (it == a.end()) ? value : it->second; +} + +// Returns map[key] if key is in map or Node::null() otherwise. +Node getNodeOrNull(const std::map<Node, Node>& map, Node key) { + std::map<Node, Node>::const_iterator it = map.find(key); + return (it == map.end()) ? Node::null() : it->second; +} + +// Returns true if for any key then a[key] <= b[key] where the value for any key +// not present is interpreted as 0. +bool isSubset(const NodeMultiset& a, const NodeMultiset& b) { + for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a) { + Node key = it_a->first; + const unsigned a_value = it_a->second; + const unsigned b_value = getCountWithDefault(b, key, 0); + if (a_value > b_value) { + return false; + } + } + return true; +} + +// Given two multisets return the multiset difference a \ b. +NodeMultiset diffMultiset(const NodeMultiset& a, const NodeMultiset& b) { + NodeMultiset difference; + for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a) { + Node key = it_a->first; + const unsigned a_value = it_a->second; + const unsigned b_value = getCountWithDefault(b, key, 0); + if (a_value > b_value) { + difference[key] = a_value - b_value; + } + } + return difference; +} + +// Return a vector containing a[key] repetitions of key in a multiset a. +std::vector<Node> ExpandMultiset(const NodeMultiset& a) { + std::vector<Node> expansion; + for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a) { + expansion.insert(expansion.end(), it_a->second, it_a->first); + } + return expansion; +} + +void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) { + Node t = QuantArith::mkCoeffTerm(coeff, x); + Trace(c) << t << " " << type << " " << rhs; +} + +struct SubstitutionConstResult { + // The resulting term of the substitution. + Node term; + + // ? + std::vector<Node> const_exp; + + // ?? + // A term sum[i] for which for rep_sum[i] not in rep_to_const. + Node variable_term; +}; /* struct SubstitutionConstResult */ + +SubstitutionConstResult getSubstitutionConst( + Node n, const std::vector<Node>& sum, const std::vector<Node>& rep_sum, + const std::map<Node, Node>& rep_to_const, + const std::map<Node, Node>& rep_to_const_exp, + const std::map<Node, Node>& rep_to_const_base) { + Assert(sum.size() == rep_sum.size()); + + SubstitutionConstResult result; + + std::vector<Node> vars; + std::vector<Node> subs; + std::set<Node> rep_exp_proc; + for (unsigned i = 0; i < rep_sum.size(); i++) { + Node cr = rep_sum[i]; + Node const_of_cr = getNodeOrNull(rep_to_const, cr); + if (const_of_cr.isNull()) { + result.variable_term = sum[i]; + continue; + } + Assert(!const_of_cr.isNull()); + Node const_base_of_cr = getNodeOrNull(rep_to_const_base, cr); + Assert(!const_base_of_cr.isNull()); + if (const_base_of_cr != sum[i]) { + result.const_exp.push_back(const_base_of_cr.eqNode(sum[i])); + } + if (rep_exp_proc.find(cr) == rep_exp_proc.end()) { + rep_exp_proc.insert(cr); + Node const_exp = getNodeOrNull(rep_to_const_exp, cr); + if (!const_exp.isNull()) { + result.const_exp.push_back(const_exp); + } + } + vars.push_back(sum[i]); + subs.push_back(const_of_cr); + } + Node substituted = + n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + result.term = Rewriter::rewrite(substituted); + return result; +} + +struct SortNonlinearExtension { + SortNonlinearExtension() + : d_nla(NULL), d_order_type(0), d_reverse_order(false) {} + NonlinearExtension* d_nla; + unsigned d_order_type; + bool d_reverse_order; + bool operator()(Node i, Node j) { + int cv = d_nla->compare(i, j, d_order_type); + if (cv == 0) { + return i < j; + } else { + return d_reverse_order ? cv < 0 : cv > 0; + } + } +}; + +bool hasNewMonomials(Node n, const std::vector<Node>& existing) { + std::set<Node> visited; + + std::vector<Node> worklist; + worklist.push_back(n); + while (!worklist.empty()) { + Node current = worklist.back(); + worklist.pop_back(); + if (!Contains(visited, current)) { + visited.insert(current); + if (current.getKind() == kind::NONLINEAR_MULT) { + if (!IsInVector(existing, current)) { + return true; + } + } else { + worklist.insert(worklist.end(), current.begin(), current.end()); + } + } + } + return false; +} + +} // namespace + +NonlinearExtension::NonlinearExtension(TheoryArith& containing, + eq::EqualityEngine* ee) + : d_lemmas(containing.getUserContext()), + d_zero_split(containing.getUserContext()), + d_containing(containing), + d_ee(ee), + d_needsLastCall(false) { + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); + d_order_points.push_back(d_neg_one); + d_order_points.push_back(d_zero); + d_order_points.push_back(d_one); +} + +NonlinearExtension::~NonlinearExtension() {} + +// Returns a reference to either map[key] if it exists in the map +// or to a default value otherwise. +// +// Warning: special care must be taken if value is a temporary object. +template <class MapType, class Key, class Value> +const Value& FindWithDefault(const MapType& map, const Key& key, + const Value& value) { + typename MapType::const_iterator it = map.find(key); + if (it == map.end()) { + return value; + } + return it->second; +} + +const NodeMultiset& NonlinearExtension::getMonomialExponentMap( + Node monomial) const { + MonomialExponentMap::const_iterator it = d_m_exp.find(monomial); + Assert(it != d_m_exp.end()); + return it->second; +} + +bool NonlinearExtension::isMonomialSubset(Node a, Node b) const { + const NodeMultiset& a_exponent_map = getMonomialExponentMap(a); + const NodeMultiset& b_exponent_map = getMonomialExponentMap(b); + + return isSubset(a_exponent_map, b_exponent_map); +} + +void NonlinearExtension::registerMonomialSubset(Node a, Node b) { + Assert(isMonomialSubset(a, b)); + + const NodeMultiset& a_exponent_map = getMonomialExponentMap(a); + const NodeMultiset& b_exponent_map = getMonomialExponentMap(b); + + std::vector<Node> diff_children = + ExpandMultiset(diffMultiset(b_exponent_map, a_exponent_map)); + Assert(!diff_children.empty()); + + d_m_contain_parent[a].push_back(b); + d_m_contain_children[b].push_back(a); + + Node mult_term = safeConstructNary(kind::MULT, diff_children); + Node nlmult_term = safeConstructNary(kind::NONLINEAR_MULT, diff_children); + d_m_contain_mult[a][b] = mult_term; + d_m_contain_umult[a][b] = nlmult_term; + Trace("nl-alg-mindex") << "..." << a << " is a subset of " << b + << ", difference is " << mult_term << std::endl; +} + +class NonLinearExtentionSubstitutionSolver { + public: + NonLinearExtentionSubstitutionSolver(const eq::EqualityEngine* ee) + : d_ee(ee) {} + + bool solve(const std::vector<Node>& vars, std::vector<Node>* subs, + std::map<Node, std::vector<Node> >* exp, + std::map<Node, std::vector<int> >* rep_to_subs_index); + + private: + bool setSubstitutionConst( + const std::vector<Node>& vars, Node r, Node r_c, Node r_cb, + const std::vector<Node>& r_c_exp, std::vector<Node>* subs, + std::map<Node, std::vector<Node> >* exp, + std::map<Node, std::vector<int> >* rep_to_subs_index); + + const eq::EqualityEngine* d_ee; + + std::map<Node, Node> d_rep_to_const; + std::map<Node, Node> d_rep_to_const_exp; + std::map<Node, Node> d_rep_to_const_base; + + // key in term_to_sum iff key in term_to_rep_sum. + std::map<Node, std::vector<Node> > d_term_to_sum; + std::map<Node, std::vector<Node> > d_term_to_rep_sum; + std::map<Node, int> d_term_to_nconst_rep_count; + + std::map<Node, std::vector<Node> > d_reps_to_parent_terms; + std::map<Node, std::vector<Node> > d_reps_to_terms; +}; + +bool NonLinearExtentionSubstitutionSolver::solve( + const std::vector<Node>& vars, std::vector<Node>* subs, + std::map<Node, std::vector<Node> >* exp, + std::map<Node, std::vector<int> >* rep_to_subs_index) { + // std::map<Node, Node> rep_to_const; + // std::map<Node, Node> rep_to_const_exp; + // std::map<Node, Node> rep_to_const_base; + + // std::map<Node, std::vector<Node> > term_to_sum; + // std::map<Node, std::vector<Node> > term_to_rep_sum; + // std::map<Node, int> term_to_nconst_rep_count; + // std::map<Node, std::vector<Node> > reps_to_parent_terms; + // std::map<Node, std::vector<Node> > reps_to_terms; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_ee); + + bool retVal = false; + while (!eqcs_i.isFinished() && !rep_to_subs_index->empty()) { + Node r = (*eqcs_i); + if (r.getType().isReal()) { + Trace("nl-subs-debug") + << "Process equivalence class " << r << "..." << std::endl; + Node r_c; + Node r_cb; + std::vector<Node> r_c_exp; + if (r.isConst()) { + r_c = r; + r_cb = r; + } + // scan the class + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_ee); + while (!eqc_i.isFinished()) { + Node n = (*eqc_i); + if (!n.isConst()) { + Trace("nl-subs-debug") << "Look at term : " << n << std::endl; + std::map<Node, Node> msum; + if (QuantArith::getMonomialSum(n, msum)) { + int nconst_count = 0; + bool evaluatable = true; + for (std::map<Node, Node>::iterator itm = msum.begin(); + itm != msum.end(); ++itm) { + if (!itm->first.isNull()) { + if (d_ee->hasTerm(itm->first)) { + Trace("nl-subs-debug") + << " ...monomial " << itm->first << std::endl; + Node cr = d_ee->getRepresentative(itm->first); + d_term_to_sum[n].push_back(itm->first); + d_term_to_rep_sum[n].push_back(cr); + if (!Contains(d_rep_to_const, cr)) { + if (!IsInVector(d_reps_to_parent_terms[cr], n)) { + d_reps_to_parent_terms[cr].push_back(n); + nconst_count++; + } + } + } else { + Trace("nl-subs-debug") + << "...is not evaluatable due to monomial " << itm->first + << std::endl; + evaluatable = false; + break; + } + } + } + if (evaluatable) { + Trace("nl-subs-debug") + << " ...term has " << nconst_count + << " unique non-constant represenative children." + << std::endl; + if (nconst_count == 0) { + if (r_c.isNull()) { + const SubstitutionConstResult result = getSubstitutionConst( + n, d_term_to_sum[n], d_term_to_rep_sum[n], d_rep_to_const, + d_rep_to_const_exp, d_rep_to_const_base); + r_c_exp.insert(r_c_exp.end(), result.const_exp.begin(), + result.const_exp.end()); + r_c = result.term; + r_cb = n; + Assert(result.variable_term.isNull()); + Assert(r_c.isConst()); + } + } else { + d_reps_to_terms[r].push_back(n); + d_term_to_nconst_rep_count[n] = nconst_count; + } + } + } else { + Trace("nl-subs-debug") + << "...could not get monomial sum " << std::endl; + } + } + ++eqc_i; + } + if (!r_c.isNull()) { + setSubstitutionConst(vars, r, r_c, r_cb, r_c_exp, subs, exp, + rep_to_subs_index); + } + } + ++eqcs_i; + } + return retVal; +} + +bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst( + const std::vector<Node>& vars, Node r, Node r_c, Node r_cb, + const std::vector<Node>& r_c_exp, std::vector<Node>* subs, + std::map<Node, std::vector<Node> >* exp, + std::map<Node, std::vector<int> >* rep_to_subs_index) { + Trace("nl-subs-debug") << "Set constant equivalence class : " << r << " -> " + << r_c << std::endl; + bool retVal = false; + + d_rep_to_const[r] = r_c; + Node expn; + if (!r_c_exp.empty()) { + expn = r_c_exp.size() == 1 + ? r_c_exp[0] + : NodeManager::currentNM()->mkNode(kind::AND, r_c_exp); + Trace("nl-subs-debug") << "...explanation is " << expn << std::endl; + d_rep_to_const_exp[r] = expn; + } + d_rep_to_const_base[r] = r_cb; + + std::map<Node, std::vector<int> >::const_iterator iti = + rep_to_subs_index->find(r); + if (iti != rep_to_subs_index->end()) { + for (unsigned i = 0; i < iti->second.size(); i++) { + int ii = iti->second[i]; + (*subs)[ii] = r_c; + std::vector<Node>& exp_var_ii = (*exp)[vars[ii]]; + exp_var_ii.clear(); + if (!expn.isNull()) { + exp_var_ii.push_back(expn); + } + if (vars[ii] != r_cb) { + exp_var_ii.push_back(vars[ii].eqNode(r_cb)); + } + } + retVal = true; + rep_to_subs_index->erase(r); + if (rep_to_subs_index->empty()) { + return retVal; + } + } + + // new inferred constants + std::map<Node, Node> new_const; + std::map<Node, std::vector<Node> > new_const_exp; + + // parent terms now evaluate to constants + std::map<Node, std::vector<Node> >::const_iterator itrp = + d_reps_to_parent_terms.find(r); + if (itrp != d_reps_to_parent_terms.end()) { + // Trace("nl-subs-debug") << "Look at " << itrp->second.size() << " parent + // terms." << std::endl; + for (unsigned i = 0; i < itrp->second.size(); i++) { + Node m = itrp->second[i]; + d_term_to_nconst_rep_count[m]--; + Node r = d_ee->getRepresentative(m); + if (d_term_to_nconst_rep_count[m] == 0) { + if (!Contains(d_rep_to_const, r)) { + Trace("nl-subs-debug") << "...parent term " << m + << " evaluates to constant." << std::endl; + if (!Contains(new_const, m)) { + const SubstitutionConstResult result = getSubstitutionConst( + m, d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const, + d_rep_to_const_exp, d_rep_to_const_base); + new_const_exp[m].insert(new_const_exp[m].end(), + result.const_exp.begin(), + result.const_exp.end()); + Node m_c = result.term; + // count should be accurate + Assert(result.variable_term.isNull()); + Assert(m_c.isConst()); + new_const[m] = m_c; + } + } + } else if (d_term_to_nconst_rep_count[m] == 1) { + // check if it is now univariate solved + if (Contains(d_rep_to_const, r)) { + Trace("nl-subs-debug") << "...parent term " << m + << " is univariate solved." << std::endl; + const SubstitutionConstResult result = getSubstitutionConst( + m, d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const, + d_rep_to_const_exp, d_rep_to_const_base); + Node eq = (result.term).eqNode(d_rep_to_const[r]); + Node v_c = QuantArith::solveEqualityFor(eq, result.variable_term); + if (!v_c.isNull()) { + Assert(v_c.isConst()); + if (Contains(new_const, result.variable_term)) { + new_const[result.variable_term] = v_c; + std::vector<Node>& explanation = + new_const_exp[result.variable_term]; + explanation.insert(explanation.end(), result.const_exp.begin(), + result.const_exp.end()); + if (m != d_rep_to_const_base[r]) { + explanation.push_back(m.eqNode(d_rep_to_const_base[r])); + } + } + } + } + } + } + } + + // equal univariate terms now solved + std::map<Node, std::vector<Node> >::iterator itt = d_reps_to_terms.find(r); + if (itt != d_reps_to_terms.end()) { + for (unsigned i = 0; i < itt->second.size(); i++) { + Node m = itt->second[i]; + if (d_term_to_nconst_rep_count[m] == 1) { + Trace("nl-subs-debug") + << "...term " << m << " is univariate solved." << std::endl; + const SubstitutionConstResult result = getSubstitutionConst( + m, d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const, + d_rep_to_const_exp, d_rep_to_const_base); + Node v = result.variable_term; + Node m_t = result.term; + Node eq = m_t.eqNode(r_c); + Node v_c = QuantArith::solveEqualityFor(eq, v); + if (!v_c.isNull()) { + Assert(v_c.isConst()); + if (new_const.find(v) == new_const.end()) { + new_const[v] = v_c; + new_const_exp[v].insert(new_const_exp[v].end(), + result.const_exp.begin(), + result.const_exp.end()); + if (m != r_cb) { + new_const_exp[v].push_back(m.eqNode(r_cb)); + } + } + } + } + } + } + + // now, process new inferred constants + for (std::map<Node, Node>::iterator itn = new_const.begin(); + itn != new_const.end(); ++itn) { + Node m = itn->first; + Node r = d_ee->getRepresentative(m); + if (!Contains(d_rep_to_const, r)) { + if (setSubstitutionConst(vars, r, itn->second, m, new_const_exp[m], subs, + exp, rep_to_subs_index)) { + retVal = true; + } + } + } + return retVal; +} + +bool NonlinearExtension::getCurrentSubstitution( + int effort, const std::vector<Node>& vars, std::vector<Node>& subs, + std::map<Node, std::vector<Node> >& exp) { + // get the constant equivalence classes + std::map<Node, std::vector<int> > rep_to_subs_index; + + bool retVal = false; + for (unsigned i = 0; i < vars.size(); i++) { + Node n = vars[i]; + if (d_ee->hasTerm(n)) { + Node nr = d_ee->getRepresentative(n); + if (nr.isConst()) { + subs.push_back(nr); + Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr + << std::endl; + exp[n].push_back(n.eqNode(nr)); + retVal = true; + } else { + rep_to_subs_index[nr].push_back(i); + subs.push_back(n); + } + } else { + subs.push_back(n); + } + } + + if (options::nlAlgSolveSubs()) { + NonLinearExtentionSubstitutionSolver substitution_solver(d_ee); + if (substitution_solver.solve(vars, &subs, &exp, &rep_to_subs_index)) { + retVal = true; + } + } + + // return true if the substitution is non-trivial + return retVal; + + // d_containing.getValuation().getModel()->getRepresentative( n ); +} + +std::pair<bool, Node> NonlinearExtension::isExtfReduced( + int effort, Node n, Node on, const std::vector<Node>& exp) const { + if (n != d_zero) { + return std::make_pair(n.getKind() != kind::NONLINEAR_MULT, Node::null()); + } + Assert(n == d_zero); + Trace("nl-alg-zero-exp") << "Infer zero : " << on << " == " << n << std::endl; + // minimize explanation + const std::set<Node> vars(on.begin(), on.end()); + + for (unsigned i = 0; i < exp.size(); i++) { + Trace("nl-alg-zero-exp") << " exp[" << i << "] = " << exp[i] << std::endl; + std::vector<Node> eqs; + if (exp[i].getKind() == kind::EQUAL) { + eqs.push_back(exp[i]); + } else if (exp[i].getKind() == kind::AND) { + for (unsigned j = 0; j < exp[i].getNumChildren(); j++) { + if (exp[i][j].getKind() == kind::EQUAL) { + eqs.push_back(exp[i][j]); + } + } + } + + for (unsigned j = 0; j < eqs.size(); j++) { + for (unsigned r = 0; r < 2; r++) { + if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) { + Trace("nl-alg-zero-exp") << "...single exp : " << eqs[j] << std::endl; + return std::make_pair(true, eqs[j]); + } + } + } + } + return std::make_pair(true, Node::null()); +} + +Node NonlinearExtension::computeModelValue(Node n, unsigned index) { + std::map<Node, Node>::iterator it = d_mv[index].find(n); + if (it != d_mv[index].end()) { + return it->second; + } else { + Trace("nl-alg-debug") << "computeModelValue " << n << std::endl; + Node ret; + if (n.isConst()) { + ret = n; + } else { + if (n.getNumChildren() == 0) { + ret = d_containing.getValuation().getModel()->getValue(n); + } else { + if (index == 1 && n.getKind() == kind::NONLINEAR_MULT) { + if (d_containing.getValuation().getModel()->hasTerm(n)) { + // use model value for abstraction + ret = d_containing.getValuation().getModel()->getRepresentative(n); + } else { + // abstraction does not exist, use concrete + ret = computeModelValue(n, 0); + } + } else { + // otherwise, compute true value + std::vector<Node> children; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back(n.getOperator()); + } + for (unsigned i = 0; i < n.getNumChildren(); i++) { + Node mc = computeModelValue(n[i], index); + children.push_back(mc); + } + ret = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(n.getKind(), children)); + if (!ret.isConst()) { + Trace("nl-alg-debug") << "...got non-constant : " << ret << " for " + << n << ", ask model directly." << std::endl; + ret = d_containing.getValuation().getModel()->getValue(ret); + } + } + } + if (ret.getType().isReal() && !isArithKind(n.getKind())) { + // Trace("nl-alg-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n + // << " ] -> " << ret << std::endl; + Assert(ret.isConst()); + } + } + Trace("nl-alg-debug") << "computed " << (index == 0 ? "M" : "M_A") << "[" + << n << "] = " << ret << std::endl; + d_mv[index][n] = ret; + return ret; + } +} + +void NonlinearExtension::registerMonomial(Node n) { + if (!IsInVector(d_monomials, n)) { + d_monomials.push_back(n); + Trace("nl-alg-debug") << "Register monomial : " << n << std::endl; + if (n.getKind() == kind::NONLINEAR_MULT) { + // get exponent count + for (unsigned k = 0; k < n.getNumChildren(); k++) { + d_m_exp[n][n[k]]++; + if (k == 0 || n[k] != n[k - 1]) { + d_m_vlist[n].push_back(n[k]); + } + } + d_m_degree[n] = n.getNumChildren(); + } else if (n == d_one) { + d_m_exp[n].clear(); + d_m_vlist[n].clear(); + d_m_degree[n] = 0; + } else { + Assert(!isArithKind(n.getKind())); + d_m_exp[n][n] = 1; + d_m_vlist[n].push_back(n); + d_m_degree[n] = 1; + } + // TODO: sort necessary here? + std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end()); + Trace("nl-alg-mindex") << "Add monomial to index : " << n << std::endl; + d_m_index.addTerm(n, d_m_vlist[n], this); + } +} + +void NonlinearExtension::setMonomialFactor(Node a, Node b, + const NodeMultiset& common) { + // Could not tell if this was being inserted intentionally or not. + std::map<Node, Node>& mono_diff_a = d_mono_diff[a]; + if (!Contains(mono_diff_a, b)) { + Trace("nl-alg-mono-factor") + << "Set monomial factor for " << a << "/" << b << std::endl; + mono_diff_a[b] = mkMonomialRemFactor(a, common); + } +} + +void NonlinearExtension::registerConstraint(Node atom) { + if (!IsInVector(d_constraints, atom)) { + d_constraints.push_back(atom); + Trace("nl-alg-debug") << "Register constraint : " << atom << std::endl; + std::map<Node, Node> msum; + if (QuantArith::getMonomialSumLit(atom, msum)) { + Trace("nl-alg-debug") << "got monomial sum: " << std::endl; + if (Trace.isOn("nl-alg-debug")) { + QuantArith::debugPrintMonomialSum(msum, "nl-alg-debug"); + } + unsigned max_degree = 0; + std::vector<Node> all_m; + std::vector<Node> max_deg_m; + for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); + ++itm) { + if (!itm->first.isNull()) { + all_m.push_back(itm->first); + registerMonomial(itm->first); + Trace("nl-alg-debug2") + << "...process monomial " << itm->first << std::endl; + Assert(d_m_degree.find(itm->first) != d_m_degree.end()); + unsigned d = d_m_degree[itm->first]; + if (d > max_degree) { + max_degree = d; + max_deg_m.clear(); + } + if (d >= max_degree) { + max_deg_m.push_back(itm->first); + } + } + } + // isolate for each maximal degree monomial + for (unsigned i = 0; i < all_m.size(); i++) { + Node m = all_m[i]; + Node rhs, coeff; + int res = QuantArith::isolate(m, msum, coeff, rhs, atom.getKind()); + if (res != 0) { + Kind type = atom.getKind(); + if (res == -1) { + type = reverseRelationKind(type); + } + Trace("nl-alg-constraint") << "Constraint : " << atom << " <=> "; + if (!coeff.isNull()) { + Trace("nl-alg-constraint") << coeff << " * "; + } + Trace("nl-alg-constraint") + << m << " " << type << " " << rhs << std::endl; + d_c_info[atom][m].d_rhs = rhs; + d_c_info[atom][m].d_coeff = coeff; + d_c_info[atom][m].d_type = type; + } + } + for (unsigned i = 0; i < max_deg_m.size(); i++) { + Node m = max_deg_m[i]; + d_c_info_maxm[atom][m] = true; + } + } else { + Trace("nl-alg-debug") << "...failed to get monomial sum." << std::endl; + } + } +} + +bool NonlinearExtension::isArithKind(Kind k) { + return k == kind::PLUS || k == kind::MULT || k == kind::NONLINEAR_MULT; +} + +Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) { + if (status == 0) { + Node a_eq_b = a.eqNode(b); + if (orderType == 0) { + return a_eq_b; + } else { + // return mkAbs( a ).eqNode( mkAbs( b ) ); + Node negate_b = NodeManager::currentNM()->mkNode(kind::UMINUS, b); + return a_eq_b.orNode(a.eqNode(negate_b)); + } + } else if (status < 0) { + return mkLit(b, a, -status); + } else { + Assert(status == 1 || status == 2); + NodeManager* nm = NodeManager::currentNM(); + Kind greater_op = status == 1 ? kind::GEQ : kind::GT; + if (orderType == 0) { + return nm->mkNode(greater_op, a, b); + } else { + // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) ); + Node zero = mkRationalNode(0); + Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, zero); + Node b_is_nonnegative = nm->mkNode(kind::GEQ, b, zero); + Node negate_a = nm->mkNode(kind::UMINUS, a); + Node negate_b = nm->mkNode(kind::UMINUS, b); + return a_is_nonnegative.iteNode( + b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b), + nm->mkNode(greater_op, a, negate_b)), + b_is_nonnegative.iteNode(nm->mkNode(greater_op, negate_a, b), + nm->mkNode(greater_op, negate_a, negate_b))); + } + } +} + +Node NonlinearExtension::mkAbs(Node a) { + if (a.isConst()) { + return mkRationalNode(a.getConst<Rational>().abs()); + } else { + NodeManager* nm = NodeManager::currentNM(); + Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, mkRationalNode(0)); + return a_is_nonnegative.iteNode(a, nm->mkNode(kind::UMINUS, a)); + } +} + +// by a <k1> b, a <k2> b, we know a <ret> b +Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) { + if (k2 < k1) { + return joinKinds(k2, k1); + } else if (k1 == k2) { + return k1; + } else { + Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ || + k1 == kind::GT || k1 == kind::GEQ); + Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ || + k2 == kind::GT || k2 == kind::GEQ); + if (k1 == kind::EQUAL) { + if (k2 == kind::LEQ || k2 == kind::GEQ) { + return k1; + } + } else if (k1 == kind::LT) { + if (k2 == kind::LEQ) { + return k1; + } + } else if (k1 == kind::LEQ) { + if (k2 == kind::GEQ) { + return kind::EQUAL; + } + } else if (k1 == kind::GT) { + if (k2 == kind::GEQ) { + return k1; + } + } + return UNDEFINED_KIND; + } +} + +// by a <k1> b, b <k2> c, we know a <ret> c +Kind NonlinearExtension::transKinds(Kind k1, Kind k2) { + if (k2 < k1) { + return transKinds(k2, k1); + } else if (k1 == k2) { + return k1; + } else { + Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ || + k1 == kind::GT || k1 == kind::GEQ); + Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ || + k2 == kind::GT || k2 == kind::GEQ); + if (k1 == kind::EQUAL) { + return k2; + } else if (k1 == kind::LT) { + if (k2 == kind::LEQ) { + return k1; + } + } else if (k1 == kind::GT) { + if (k2 == kind::GEQ) { + return k1; + } + } + return UNDEFINED_KIND; + } +} + +Node NonlinearExtension::mkMonomialRemFactor( + Node n, const NodeMultiset& n_exp_rem) const { + std::vector<Node> children; + const NodeMultiset& exponent_map = getMonomialExponentMap(n); + for (NodeMultiset::const_iterator itme2 = exponent_map.begin(); + itme2 != exponent_map.end(); ++itme2) { + Node v = itme2->first; + unsigned inc = itme2->second; + Trace("nl-alg-mono-factor") + << "..." << inc << " factors of " << v << std::endl; + unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0); + Assert(count_in_n_exp_rem <= inc); + inc -= count_in_n_exp_rem; + Trace("nl-alg-mono-factor") + << "......rem, now " << inc << " factors of " << v << std::endl; + children.insert(children.end(), inc, v); + } + Node ret = safeConstructNary(kind::MULT, children); + ret = Rewriter::rewrite(ret); + Trace("nl-alg-mono-factor") << "...return : " << ret << std::endl; + return ret; +} + +int NonlinearExtension::flushLemma(Node lem) { + Trace("nl-alg-lemma-debug") + << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl; + lem = Rewriter::rewrite(lem); + if (Contains(d_lemmas, lem)) { + Trace("nl-alg-lemma-debug") + << "NonlinearExtension::Lemma duplicate : " << lem << std::endl; + // should not generate duplicates + // Assert( false ); + return 0; + } + d_lemmas.insert(lem); + Trace("nl-alg-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; + d_containing.getOutputChannel().lemma(lem); + return 1; +} + +int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) { + if (options::nlAlgEntailConflicts()) { + // check if any are entailed to be false + for (unsigned i = 0; i < lemmas.size(); i++) { + Node ch_lemma = lemmas[i].negate(); + ch_lemma = Rewriter::rewrite(ch_lemma); + Trace("nl-alg-et-debug") + << "Check entailment of " << ch_lemma << "..." << std::endl; + std::pair<bool, Node> et = d_containing.getValuation().entailmentCheck( + THEORY_OF_TYPE_BASED, ch_lemma); + Trace("nl-alg-et-debug") << "entailment test result : " << et.first << " " + << et.second << std::endl; + if (et.first) { + Trace("nl-alg-et") << "*** Lemma entailed to be in conflict : " + << lemmas[i] << std::endl; + // return just this lemma + if (flushLemma(lemmas[i])) { + lemmas.clear(); + return 1; + } + } + } + } + + int sum = 0; + for (unsigned i = 0; i < lemmas.size(); i++) { + sum += flushLemma(lemmas[i]); + } + lemmas.clear(); + return sum; +} + +std::set<Node> NonlinearExtension::getFalseInModel( + const std::vector<Node>& assertions) { + std::set<Node> false_asserts; + for (size_t i = 0; i < assertions.size(); ++i) { + Node lit = assertions[i]; + Node litv = computeModelValue(lit); + Trace("nl-alg-mv") << "M[[ " << lit << " ]] -> " << litv; + if (litv != d_true) { + Trace("nl-alg-mv") << " [model-false]" << std::endl; + Assert(litv == d_false); + false_asserts.insert(lit); + } else { + Trace("nl-alg-mv") << std::endl; + } + } + return false_asserts; +} + +std::vector<Node> NonlinearExtension::splitOnZeros( + const std::vector<Node>& ms_vars) { + std::vector<Node> lemmas; + if (!options::nlAlgSplitZero()) { + return lemmas; + } + for (unsigned i = 0; i < ms_vars.size(); i++) { + Node v = ms_vars[i]; + if (d_zero_split.insert(v)) { + Node lem = v.eqNode(d_zero); + lem = Rewriter::rewrite(lem); + d_containing.getValuation().ensureLiteral(lem); + d_containing.getOutputChannel().requirePhase(lem, true); + lem = NodeManager::currentNM()->mkNode(kind::OR, lem, lem.negate()); + lemmas.push_back(lem); + } + } + return lemmas; +} + +void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, + const std::set<Node>& false_asserts) { + // processed monomials + std::map<Node, bool> ms_proc; + + // list of monomials + std::vector<Node> ms; + d_containing.getExtTheory()->getTerms(ms); + // list of variables occurring in monomials + std::vector<Node> ms_vars; + + // register monomials + Trace("nl-alg-mv") << "Monomials : " << std::endl; + for (unsigned j = 0; j < ms.size(); j++) { + Node a = ms[j]; + registerMonomial(a); + computeModelValue(a, 0); + computeModelValue(a, 1); + Assert(d_mv[1][a].isConst()); + Assert(d_mv[0][a].isConst()); + Trace("nl-alg-mv") << " " << a << " -> " << d_mv[1][a] << " [" + << d_mv[0][a] << "]" << std::endl; + + std::map<Node, std::vector<Node> >::iterator itvl = d_m_vlist.find(a); + Assert(itvl != d_m_vlist.end()); + for (unsigned k = 0; k < itvl->second.size(); k++) { + if (!IsInVector(ms_vars, itvl->second[k])) { + ms_vars.push_back(itvl->second[k]); + } + } + /* + //mark processed if has a "one" factor (will look at reduced monomial) + std::map< Node, std::map< Node, unsigned > >::iterator itme = + d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node, + unsigned >::iterator itme2 = itme->second.begin(); itme2 != + itme->second.end(); ++itme2 ){ Node v = itme->first; Assert( + d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if( + mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true; + Trace("nl-alg-mv") + << "...mark " << a << " reduced since has 1 factor." << std::endl; + break; + } + } + */ + } + + // register constants + registerMonomial(d_one); + for (unsigned j = 0; j < d_order_points.size(); j++) { + Node c = d_order_points[j]; + computeModelValue(c, 0); + computeModelValue(c, 1); + } + + int lemmas_proc; + std::vector<Node> lemmas; + + // register variables + Trace("nl-alg-mv") << "Variables : " << std::endl; + Trace("nl-alg") << "Get zero split lemmas..." << std::endl; + for (unsigned i = 0; i < ms_vars.size(); i++) { + Node v = ms_vars[i]; + registerMonomial(v); + computeModelValue(v, 0); + computeModelValue(v, 1); + Trace("nl-alg-mv") << " " << v << " -> " << d_mv[0][v] << std::endl; + } + + // possibly split on zero? + lemmas = splitOnZeros(ms_vars); + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + << std::endl; + return; + } + + //-----------------------------------lemmas based on sign (comparison to zero) + std::map<Node, int> signs; + Trace("nl-alg") << "Get sign lemmas..." << std::endl; + for (unsigned j = 0; j < ms.size(); j++) { + Node a = ms[j]; + if (ms_proc.find(a) == ms_proc.end()) { + std::vector<Node> exp; + Trace("nl-alg-debug") << " process " << a << "..." << std::endl; + signs[a] = compareSign(a, a, 0, 1, exp, lemmas); + if (signs[a] == 0) { + ms_proc[a] = true; + Trace("nl-alg-mv") << "...mark " << a + << " reduced since its value is 0." << std::endl; + } + } + } + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + << std::endl; + return; + } + + //-----------------------------lemmas based on magnitude of non-zero monomials + for (unsigned r = 1; r <= 1; r++) { + assignOrderIds(ms_vars, d_order_vars[r], r); + + // sort individual variable lists + SortNonlinearExtension smv; + smv.d_nla = this; + smv.d_order_type = r; + smv.d_reverse_order = true; + for (unsigned j = 0; j < ms.size(); j++) { + std::sort(d_m_vlist[ms[j]].begin(), d_m_vlist[ms[j]].end(), smv); + } + for (unsigned c = 0; c < 3; c++) { + // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L + // in lemmas + std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers; + Trace("nl-alg") << "Get comparison lemmas (order=" << r + << ", compare=" << c << ")..." << std::endl; + for (unsigned j = 0; j < ms.size(); j++) { + Node a = ms[j]; + if (ms_proc.find(a) == ms_proc.end()) { + if (c == 0) { + // compare magnitude against 1 + std::vector<Node> exp; + NodeMultiset a_exp_proc; + NodeMultiset b_exp_proc; + compareMonomial(a, a, a_exp_proc, d_one, d_one, b_exp_proc, exp, + lemmas, cmp_infers); + } else { + std::map<Node, NodeMultiset>::iterator itmea = d_m_exp.find(a); + Assert(itmea != d_m_exp.end()); + if (c == 1) { + // TODO : not just against containing variables? + // compare magnitude against variables + for (unsigned k = 0; k < ms_vars.size(); k++) { + Node v = ms_vars[k]; + std::vector<Node> exp; + NodeMultiset a_exp_proc; + NodeMultiset b_exp_proc; + if (itmea->second.find(v) != itmea->second.end()) { + a_exp_proc[v] = 1; + b_exp_proc[v] = 1; + setMonomialFactor(a, v, a_exp_proc); + setMonomialFactor(v, a, b_exp_proc); + compareMonomial(a, a, a_exp_proc, v, v, b_exp_proc, exp, + lemmas, cmp_infers); + } + } + } else { + // compare magnitude against other non-linear monomials + for (unsigned k = (j + 1); k < ms.size(); k++) { + Node b = ms[k]; + //(signs[a]==signs[b])==(r==0) + if (ms_proc.find(b) == ms_proc.end()) { + std::map<Node, NodeMultiset>::iterator itmeb = + d_m_exp.find(b); + Assert(itmeb != d_m_exp.end()); + + std::vector<Node> exp; + // take common factors of monomials, set minimum of + // common exponents as processed + NodeMultiset a_exp_proc; + NodeMultiset b_exp_proc; + for (NodeMultiset::iterator itmea2 = itmea->second.begin(); + itmea2 != itmea->second.end(); ++itmea2) { + NodeMultiset::iterator itmeb2 = + itmeb->second.find(itmea2->first); + if (itmeb2 != itmeb->second.end()) { + unsigned min_exp = itmea2->second > itmeb2->second + ? itmeb2->second + : itmea2->second; + a_exp_proc[itmea2->first] = min_exp; + b_exp_proc[itmea2->first] = min_exp; + Trace("nl-alg-comp") + << "Common exponent : " << itmea2->first << " : " + << min_exp << std::endl; + } + } + if (!a_exp_proc.empty()) { + setMonomialFactor(a, b, a_exp_proc); + setMonomialFactor(b, a, b_exp_proc); + } + /* + if( !a_exp_proc.empty() ){ + //reduction based on common exponents a > 0 => ( a * b + <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b + !<> c ) ? }else{ compareMonomial( a, a, a_exp_proc, b, + b, b_exp_proc, exp, lemmas ); + } + */ + compareMonomial(a, a, a_exp_proc, b, b, b_exp_proc, exp, + lemmas, cmp_infers); + } + } + } + } + } + } + // remove redundant lemmas, e.g. if a > b, b > c, a > c were + // inferred, discard lemma with conclusion a > c + Trace("nl-alg-comp") << "Compute redundancies for " << lemmas.size() + << " lemmas." << std::endl; + // naive + std::vector<Node> r_lemmas; + for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb = + cmp_infers.begin(); + itb != cmp_infers.end(); ++itb) { + for (std::map<Node, std::map<Node, Node> >::iterator itc = + itb->second.begin(); + itc != itb->second.end(); ++itc) { + for (std::map<Node, Node>::iterator itc2 = itc->second.begin(); + itc2 != itc->second.end(); ++itc2) { + std::map<Node, bool> visited; + for (std::map<Node, Node>::iterator itc3 = itc->second.begin(); + itc3 != itc->second.end(); ++itc3) { + if (itc3->first != itc2->first) { + std::vector<Node> exp; + if (cmp_holds(itc3->first, itc2->first, itb->second, exp, + visited)) { + r_lemmas.push_back(itc2->second); + Trace("nl-alg-comp") + << "...inference of " << itc->first << " > " + << itc2->first << " was redundant." << std::endl; + break; + } + } + } + } + } + } + std::vector<Node> nr_lemmas; + for (unsigned i = 0; i < lemmas.size(); i++) { + if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) == + r_lemmas.end()) { + nr_lemmas.push_back(lemmas[i]); + } + } + // TODO: only take maximal lower/minimial lower bounds? + + Trace("nl-alg-comp") << nr_lemmas.size() << " / " << lemmas.size() + << " were non-redundant." << std::endl; + lemmas_proc = flushLemmas(nr_lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc + << " new lemmas (out of possible " << lemmas.size() + << ")." << std::endl; + return; + } + } + } + + // sort monomials by degree + SortNonlinearExtension snlad; + snlad.d_nla = this; + snlad.d_order_type = 4; + snlad.d_reverse_order = false; + std::sort(ms.begin(), ms.end(), snlad); + // all monomials + std::vector<Node> terms; + terms.insert(terms.end(), ms_vars.begin(), ms_vars.end()); + terms.insert(terms.end(), ms.begin(), ms.end()); + + // term -> coeff -> rhs -> ( status, exp, b ), + // where we have that : exp => ( coeff * term <status> rhs ) + // b is true if degree( term ) >= degree( rhs ) + std::map<Node, std::map<Node, std::map<Node, Kind> > > ci; + std::map<Node, std::map<Node, std::map<Node, Node> > > ci_exp; + std::map<Node, std::map<Node, std::map<Node, bool> > > ci_max; + + // If ( m, p1, true ), then it would help satisfiability if m were ( > + // if p1=true, < if p1=false ) + std::map<Node, std::map<bool, bool> > tplane_refine_dir; + + // register constraints + Trace("nl-alg-debug") << "Register bound constraints..." << std::endl; + for (context::CDList<Assertion>::const_iterator it = + d_containing.facts_begin(); + it != d_containing.facts_end(); ++it) { + Node lit = (*it).assertion; + bool polarity = lit.getKind() != kind::NOT; + Node atom = lit.getKind() == kind::NOT ? lit[0] : lit; + registerConstraint(atom); + bool is_false_lit = false_asserts.find(lit) != false_asserts.end(); + // add information about bounds to variables + std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc = + d_c_info.find(atom); + std::map<Node, std::map<Node, bool> >::iterator itcm = + d_c_info_maxm.find(atom); + if (itc != d_c_info.end()) { + Assert(itcm != d_c_info_maxm.end()); + for (std::map<Node, ConstraintInfo>::iterator itcc = itc->second.begin(); + itcc != itc->second.end(); ++itcc) { + Node x = itcc->first; + Node coeff = itcc->second.d_coeff; + Node rhs = itcc->second.d_rhs; + Kind type = itcc->second.d_type; + Node exp = lit; + if (!polarity) { + // reverse + if (type == kind::EQUAL) { + // we will take the strict inequality in the direction of the + // model + Node lhs = QuantArith::mkCoeffTerm(coeff, x); + Node query = NodeManager::currentNM()->mkNode(kind::GT, lhs, rhs); + Node query_mv = computeModelValue(query, 1); + if (query_mv == d_true) { + exp = query; + type = kind::GT; + } else { + Assert(query_mv == d_false); + exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs); + type = kind::LT; + } + } else { + type = negateKind(type); + } + } + // add to status if maximal degree + ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end(); + if (Trace.isOn("nl-alg-bound-debug2")) { + Node t = QuantArith::mkCoeffTerm(coeff, x); + Trace("nl-alg-bound-debug2") + << "Add Bound: " << t << " " << type << " " << rhs << " by " + << exp << std::endl; + } + bool updated = true; + std::map<Node, Kind>::iterator its = ci[x][coeff].find(rhs); + if (its == ci[x][coeff].end()) { + ci[x][coeff][rhs] = type; + ci_exp[x][coeff][rhs] = exp; + } else if (type != its->second) { + Trace("nl-alg-bound-debug2") + << "Joining kinds : " << type << " " << its->second << std::endl; + Kind jk = joinKinds(type, its->second); + if (jk == kind::UNDEFINED_KIND) { + updated = false; + } else if (jk != its->second) { + if (jk == type) { + ci[x][coeff][rhs] = type; + ci_exp[x][coeff][rhs] = exp; + } else { + ci[x][coeff][rhs] = jk; + ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode( + kind::AND, ci_exp[x][coeff][rhs], exp); + } + } else { + updated = false; + } + } + if (Trace.isOn("nl-alg-bound")) { + if (updated) { + Trace("nl-alg-bound") << "Bound: "; + debugPrintBound("nl-alg-bound", coeff, x, ci[x][coeff][rhs], rhs); + Trace("nl-alg-bound") << " by " << ci_exp[x][coeff][rhs]; + if (ci_max[x][coeff][rhs]) { + Trace("nl-alg-bound") << ", is max degree"; + } + Trace("nl-alg-bound") << std::endl; + } + } + // compute if bound is not satisfied, and store what is required + // for a possible refinement + if (options::nlAlgTangentPlanes()) { + if (is_false_lit) { + Node rhs_v = computeModelValue(rhs, 0); + Node x_v = computeModelValue(x, 0); + bool needsRefine = false; + bool refineDir; + if (rhs_v == x_v) { + if (type == kind::GT) { + needsRefine = true; + refineDir = true; + } else if (type == kind::LT) { + needsRefine = true; + refineDir = false; + } + } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) { + if (type != kind::GT && type != kind::GEQ) { + needsRefine = true; + refineDir = false; + } + } else { + if (type != kind::LT && type != kind::LEQ) { + needsRefine = true; + refineDir = true; + } + } + Trace("nl-alg-tplanes-cons-debug") + << "...compute if bound corresponds to a required " + "refinement" + << std::endl; + Trace("nl-alg-tplanes-cons-debug") + << "...M[" << x << "] = " << x_v << ", M[" << rhs + << "] = " << rhs_v << std::endl; + Trace("nl-alg-tplanes-cons-debug") << "...refine = " << needsRefine + << "/" << refineDir << std::endl; + if (needsRefine) { + Trace("nl-alg-tplanes-cons") + << "---> By " << lit << " and since M[" << x << "] = " << x_v + << ", M[" << rhs << "] = " << rhs_v << ", "; + Trace("nl-alg-tplanes-cons") + << "monomial " << x << " should be " + << (refineDir ? "larger" : "smaller") << std::endl; + tplane_refine_dir[x][refineDir] = true; + } + } + } + } + } + } + // reflexive constraints + Node null_coeff; + for (unsigned j = 0; j < terms.size(); j++) { + Node n = terms[j]; + ci[n][null_coeff][n] = kind::EQUAL; + ci_exp[n][null_coeff][n] = d_true; + ci_max[n][null_coeff][n] = false; + } + + //-----------------------------------------------------------------------------------------inferred + // bounds lemmas, e.g. x >= t => y*x >= y*t + Trace("nl-alg") << "Get inferred bound lemmas..." << std::endl; + + std::vector<Node> nt_lemmas; + for (unsigned k = 0; k < terms.size(); k++) { + Node x = terms[k]; + Trace("nl-alg-bound-debug") + << "Process bounds for " << x << " : " << std::endl; + std::map<Node, std::vector<Node> >::iterator itm = + d_m_contain_parent.find(x); + if (itm != d_m_contain_parent.end()) { + Trace("nl-alg-bound-debug") << "...has " << itm->second.size() + << " parent monomials." << std::endl; + // check derived bounds + std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc = + ci.find(x); + if (itc != ci.end()) { + for (std::map<Node, std::map<Node, Kind> >::iterator itcc = + itc->second.begin(); + itcc != itc->second.end(); ++itcc) { + Node coeff = itcc->first; + Node t = QuantArith::mkCoeffTerm(coeff, x); + for (std::map<Node, Kind>::iterator itcr = itcc->second.begin(); + itcr != itcc->second.end(); ++itcr) { + Node rhs = itcr->first; + // only consider this bound if maximal degree + if (ci_max[x][coeff][rhs]) { + Kind type = itcr->second; + for (unsigned j = 0; j < itm->second.size(); j++) { + Node y = itm->second[j]; + Assert(d_m_contain_mult[x].find(y) != + d_m_contain_mult[x].end()); + Node mult = d_m_contain_mult[x][y]; + // x <k> t => m*x <k'> t where y = m*x + // get the sign of mult + Node mmv = computeModelValue(mult); + Trace("nl-alg-bound-debug2") + << "Model value of " << mult << " is " << mmv << std::endl; + Assert(mmv.isConst()); + int mmv_sign = mmv.getConst<Rational>().sgn(); + Trace("nl-alg-bound-debug2") + << " sign of " << mmv << " is " << mmv_sign << std::endl; + if (mmv_sign != 0) { + Trace("nl-alg-bound-debug") + << " from " << x << " * " << mult << " = " << y + << " and " << t << " " << type << " " << rhs + << ", infer : " << std::endl; + Kind infer_type = + mmv_sign == -1 ? reverseRelationKind(type) : type; + Node infer_lhs = + NodeManager::currentNM()->mkNode(kind::MULT, mult, t); + Node infer_rhs = + NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs); + Node infer = NodeManager::currentNM()->mkNode( + infer_type, infer_lhs, infer_rhs); + Trace("nl-alg-bound-debug") << " " << infer << std::endl; + infer = Rewriter::rewrite(infer); + Trace("nl-alg-bound-debug2") + << " ...rewritten : " << infer << std::endl; + // check whether it is false in model for abstraction + Node infer_mv = computeModelValue(infer, 1); + Trace("nl-alg-bound-debug") + << " ...infer model value is " << infer_mv + << std::endl; + if (infer_mv == d_false) { + Node exp = NodeManager::currentNM()->mkNode( + kind::AND, + NodeManager::currentNM()->mkNode( + mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero), + ci_exp[x][coeff][rhs]); + Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES, + exp, infer); + Node pr_iblem = iblem; + iblem = Rewriter::rewrite(iblem); + bool introNewTerms = hasNewMonomials(iblem, ms); + Trace("nl-alg-bound-lemma") + << "*** Bound inference lemma : " << iblem + << " (pre-rewrite : " << pr_iblem << ")" << std::endl; + // Trace("nl-alg-bound-lemma") << " intro new + // monomials = " << introNewTerms << std::endl; + if (!introNewTerms) { + lemmas.push_back(iblem); + } else { + nt_lemmas.push_back(iblem); + } + } + } else { + Trace("nl-alg-bound-debug") << " ...coefficient " << mult + << " is zero." << std::endl; + } + } + } + } + } + } + } else { + Trace("nl-alg-bound-debug") << "...has no parent monomials." << std::endl; + } + } + // Trace("nl-alg") << "Bound lemmas : " << lemmas.size() << ", " << + // nt_lemmas.size() << std::endl; prioritize lemmas that do not + // introduce new monomials + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + << std::endl; + return; + } + + //------------------------------------resolution bound inferences, e.g. + //( + // y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t + if (options::nlAlgResBound()) { + Trace("nl-alg") << "Get resolution inferred bound lemmas..." << std::endl; + for (unsigned j = 0; j < terms.size(); j++) { + Node a = terms[j]; + std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca = + ci.find(a); + if (itca != ci.end()) { + for (unsigned k = (j + 1); k < terms.size(); k++) { + Node b = terms[k]; + std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator + itcb = ci.find(b); + if (itcb != ci.end()) { + Trace("nl-alg-rbound-debug") << "resolution inferences : compare " + << a << " and " << b << std::endl; + // if they have common factors + std::map<Node, Node>::iterator ita = d_mono_diff[a].find(b); + if (ita != d_mono_diff[a].end()) { + std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a); + Assert(itb != d_mono_diff[b].end()); + Node mv_a = computeModelValue(ita->second, 1); + Assert(mv_a.isConst()); + int mv_a_sgn = mv_a.getConst<Rational>().sgn(); + Assert(mv_a_sgn != 0); + Node mv_b = computeModelValue(itb->second, 1); + Assert(mv_b.isConst()); + int mv_b_sgn = mv_b.getConst<Rational>().sgn(); + Assert(mv_b_sgn != 0); + Trace("nl-alg-rbound") << "Get resolution inferences for [a] " + << a << " vs [b] " << b << std::endl; + Trace("nl-alg-rbound") + << " [a] factor is " << ita->second + << ", sign in model = " << mv_a_sgn << std::endl; + Trace("nl-alg-rbound") + << " [b] factor is " << itb->second + << ", sign in model = " << mv_b_sgn << std::endl; + + std::vector<Node> exp; + // bounds of a + for (std::map<Node, std::map<Node, Kind> >::iterator itcac = + itca->second.begin(); + itcac != itca->second.end(); ++itcac) { + Node coeff_a = itcac->first; + for (std::map<Node, Kind>::iterator itcar = + itcac->second.begin(); + itcar != itcac->second.end(); ++itcar) { + Node rhs_a = itcar->first; + Node rhs_a_res_base = NodeManager::currentNM()->mkNode( + kind::MULT, itb->second, rhs_a); + rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base); + if (!hasNewMonomials(rhs_a_res_base, ms)) { + Kind type_a = itcar->second; + exp.push_back(ci_exp[a][coeff_a][rhs_a]); + + // bounds of b + for (std::map<Node, std::map<Node, Kind> >::iterator itcbc = + itcb->second.begin(); + itcbc != itcb->second.end(); ++itcbc) { + Node coeff_b = itcbc->first; + Node rhs_a_res = + QuantArith::mkCoeffTerm(coeff_b, rhs_a_res_base); + for (std::map<Node, Kind>::iterator itcbr = + itcbc->second.begin(); + itcbr != itcbc->second.end(); ++itcbr) { + Node rhs_b = itcbr->first; + Node rhs_b_res = NodeManager::currentNM()->mkNode( + kind::MULT, ita->second, rhs_b); + rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res); + rhs_b_res = Rewriter::rewrite(rhs_b_res); + if (!hasNewMonomials(rhs_b_res, ms)) { + Kind type_b = itcbr->second; + exp.push_back(ci_exp[b][coeff_b][rhs_b]); + if (Trace.isOn("nl-alg-rbound")) { + Trace("nl-alg-rbound") << "* try bounds : "; + debugPrintBound("nl-alg-rbound", coeff_a, a, type_a, + rhs_a); + Trace("nl-alg-rbound") << std::endl; + Trace("nl-alg-rbound") << " "; + debugPrintBound("nl-alg-rbound", coeff_b, b, type_b, + rhs_b); + Trace("nl-alg-rbound") << std::endl; + } + Kind types[2]; + for (unsigned r = 0; r < 2; r++) { + Node pivot_factor = + r == 0 ? itb->second : ita->second; + int pivot_factor_sign = + r == 0 ? mv_b_sgn : mv_a_sgn; + types[r] = r == 0 ? type_a : type_b; + if (pivot_factor_sign == (r == 0 ? 1 : -1)) { + types[r] = reverseRelationKind(types[r]); + } + if (pivot_factor_sign == 1) { + exp.push_back(NodeManager::currentNM()->mkNode( + kind::GT, pivot_factor, d_zero)); + } else { + exp.push_back(NodeManager::currentNM()->mkNode( + kind::LT, pivot_factor, d_zero)); + } + } + Kind jk = transKinds(types[0], types[1]); + Trace("nl-alg-rbound-debug") + << "trans kind : " << types[0] << " + " + << types[1] << " = " << jk << std::endl; + if (jk != kind::UNDEFINED_KIND) { + Node conc = NodeManager::currentNM()->mkNode( + jk, rhs_a_res, rhs_b_res); + Node conc_mv = computeModelValue(conc, 1); + if (conc_mv == d_false) { + Node rblem = NodeManager::currentNM()->mkNode( + kind::IMPLIES, + NodeManager::currentNM()->mkNode(kind::AND, + exp), + conc); + Trace("nl-alg-rbound-lemma-debug") + << "Resolution bound lemma " + "(pre-rewrite) " + ": " + << rblem << std::endl; + rblem = Rewriter::rewrite(rblem); + Trace("nl-alg-rbound-lemma") + << "Resolution bound lemma : " << rblem + << std::endl; + lemmas.push_back(rblem); + } + } + exp.pop_back(); + exp.pop_back(); + exp.pop_back(); + } + } + } + exp.pop_back(); + } + } + } + } + } + } + } + } + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + << std::endl; + return; + } + } + + // from inferred bound inferences + lemmas_proc = flushLemmas(nt_lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc + << " new (monomial-introducing) lemmas." << std::endl; + return; + } + + if (options::nlAlgTangentPlanes()) { + Trace("nl-alg") << "Get tangent plane lemmas..." << std::endl; + unsigned kstart = ms_vars.size(); + for (unsigned k = kstart; k < terms.size(); k++) { + Node t = terms[k]; + // if this term requires a refinement + if (tplane_refine_dir.find(t) != tplane_refine_dir.end()) { + Trace("nl-alg-tplanes") + << "Look at monomial requiring refinement : " << t << std::endl; + // get a decomposition + std::map<Node, std::vector<Node> >::iterator it = + d_m_contain_children.find(t); + if (it != d_m_contain_children.end()) { + std::map<Node, std::map<Node, bool> > dproc; + for (unsigned j = 0; j < it->second.size(); j++) { + Node tc = it->second[j]; + if (tc != d_one) { + Node tc_diff = d_m_contain_umult[tc][t]; + Assert(!tc_diff.isNull()); + Node a = tc < tc_diff ? tc : tc_diff; + Node b = tc < tc_diff ? tc_diff : tc; + if (dproc[a].find(b) == dproc[a].end()) { + dproc[a][b] = true; + Trace("nl-alg-tplanes") + << " decomposable into : " << a << " * " << b << std::endl; + Node a_v = computeModelValue(a, 1); + Node b_v = computeModelValue(b, 1); + // tangent plane + Node tplane = NodeManager::currentNM()->mkNode( + kind::MINUS, + NodeManager::currentNM()->mkNode( + kind::PLUS, + NodeManager::currentNM()->mkNode(kind::MULT, b_v, a), + NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)), + NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v)); + for (unsigned d = 0; d < 4; d++) { + Node aa = NodeManager::currentNM()->mkNode( + d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v); + Node ab = NodeManager::currentNM()->mkNode( + d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v); + Node conc = NodeManager::currentNM()->mkNode( + d <= 1 ? kind::LEQ : kind::GEQ, t, tplane); + Node tlem = NodeManager::currentNM()->mkNode( + kind::OR, aa.negate(), ab.negate(), conc); + Trace("nl-alg-tplanes") + << "Tangent plane lemma : " << tlem << std::endl; + lemmas.push_back(tlem); + } + } + } + } + } + } + } + Trace("nl-alg") << "...trying " << lemmas.size() + << " tangent plane lemmas..." << std::endl; + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + << std::endl; + return; + } + } + + Trace("nl-alg") << "...set incomplete" << std::endl; + d_containing.getOutputChannel().setIncomplete(); +} + +void NonlinearExtension::check(Theory::Effort e) { + Trace("nl-alg") << std::endl; + Trace("nl-alg") << "NonlinearExtension::check, effort = " << e << std::endl; + if (e == Theory::EFFORT_FULL) { + d_containing.getExtTheory()->clearCache(); + d_needsLastCall = true; + if (options::nlAlgRewrites()) { + std::vector<Node> nred; + if (!d_containing.getExtTheory()->doInferences(0, nred)) { + Trace("nl-alg") << "...sent no lemmas, # extf to reduce = " + << nred.size() << std::endl; + if (nred.empty()) { + d_needsLastCall = false; + } + } else { + Trace("nl-alg") << "...sent lemmas." << std::endl; + } + } + } else { + Assert(e == Theory::EFFORT_LAST_CALL); + Trace("nl-alg-mv") << "Getting model values... check for [model-false]" + << std::endl; + d_mv[0].clear(); + d_mv[1].clear(); + std::vector<Node> assertions; + for (Theory::assertions_iterator it = d_containing.facts_begin(); + it != d_containing.facts_end(); ++it) { + const Assertion& assertion = *it; + assertions.push_back(assertion.assertion); + } + const std::set<Node> false_asserts = getFalseInModel(assertions); + if (!false_asserts.empty()) { + checkLastCall(assertions, false_asserts); + } + } +} + +void NonlinearExtension::assignOrderIds(std::vector<Node>& vars, + NodeMultiset& order, + unsigned orderType) { + SortNonlinearExtension smv; + smv.d_nla = this; + smv.d_order_type = orderType; + smv.d_reverse_order = false; + std::sort(vars.begin(), vars.end(), smv); + + order.clear(); + // assign ordering id's + unsigned counter = 0; + unsigned order_index = (orderType == 0 || orderType == 2) ? 0 : 1; + Node prev; + for (unsigned j = 0; j < vars.size(); j++) { + Node x = vars[j]; + Node v = get_compare_value(x, orderType); + Trace("nl-alg-mvo") << " order " << x << " : " << v << std::endl; + if (v != prev) { + // builtin points + bool success; + do { + success = false; + if (order_index < d_order_points.size()) { + Node vv = get_compare_value(d_order_points[order_index], orderType); + if (compare_value(v, vv, orderType) <= 0) { + counter++; + Trace("nl-alg-mvo") + << "O_" << orderType << "[" << d_order_points[order_index] + << "] = " << counter << std::endl; + order[d_order_points[order_index]] = counter; + prev = vv; + order_index++; + success = true; + } + } + } while (success); + } + if (prev.isNull() || compare_value(v, prev, orderType) != 0) { + counter++; + } + Trace("nl-alg-mvo") << "O_" << orderType << "[" << x << "] = " << counter + << std::endl; + order[x] = counter; + prev = v; + } + while (order_index < d_order_points.size()) { + counter++; + Trace("nl-alg-mvo") << "O_" << orderType << "[" + << d_order_points[order_index] << "] = " << counter + << std::endl; + order[d_order_points[order_index]] = counter; + order_index++; + } +} + +int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const { + Assert(orderType >= 0); + if (orderType <= 3) { + return compare_value(get_compare_value(i, orderType), + get_compare_value(j, orderType), orderType); + // minimal degree + } else if (orderType == 4) { + unsigned i_count = getCount(d_m_degree, i); + unsigned j_count = getCount(d_m_degree, j); + return i_count == j_count ? 0 : (i_count < j_count ? 1 : -1); + } else { + return 0; + } +} + +int NonlinearExtension::compare_value(Node i, Node j, + unsigned orderType) const { + Assert(orderType >= 0 && orderType <= 3); + Trace("nl-alg-debug") << "compare_value " << i << " " << j + << ", o = " << orderType << std::endl; + int ret; + if (i == j) { + ret = 0; + } else if (orderType == 0 || orderType == 2) { + ret = i.getConst<Rational>() < j.getConst<Rational>() ? 1 : -1; + } else { + Trace("nl-alg-debug") << "vals : " << i.getConst<Rational>() << " " + << j.getConst<Rational>() << std::endl; + Trace("nl-alg-debug") << i.getConst<Rational>().abs() << " " + << j.getConst<Rational>().abs() << std::endl; + ret = (i.getConst<Rational>().abs() == j.getConst<Rational>().abs() + ? 0 + : (i.getConst<Rational>().abs() < j.getConst<Rational>().abs() + ? 1 + : -1)); + } + Trace("nl-alg-debug") << "...return " << ret << std::endl; + return ret; +} + +Node NonlinearExtension::get_compare_value(Node i, unsigned orderType) const { + Trace("nl-alg-debug") << "Compare variable " << i << " " << orderType + << std::endl; + Assert(orderType >= 0 && orderType <= 3); + unsigned mindex = orderType <= 1 ? 0 : 1; + std::map<Node, Node>::const_iterator iti = d_mv[mindex].find(i); + Assert(iti != d_mv[mindex].end()); + return iti->second; +} + +// trying to show a <> 0 by inequalities between variables in monomial a w.r.t +// 0 +int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, + int status, std::vector<Node>& exp, + std::vector<Node>& lem) { + Trace("nl-alg-debug") << "Process " << a << " at index " << a_index + << ", status is " << status << std::endl; + Assert(d_mv[1].find(oa) != d_mv[1].end()); + if (a_index == d_m_vlist[a].size()) { + if (d_mv[1][oa].getConst<Rational>().sgn() != status) { + Node lemma = safeConstructNary(kind::AND, exp) + .impNode(mkLit(oa, d_zero, status * 2)); + lem.push_back(lemma); + } + return status; + } else { + Assert(a_index < d_m_vlist[a].size()); + Node av = d_m_vlist[a][a_index]; + unsigned aexp = d_m_exp[a][av]; + // take current sign in model + Assert(d_mv[0].find(av) != d_mv[0].end()); + int sgn = d_mv[0][av].getConst<Rational>().sgn(); + Trace("nl-alg-debug") << "Process var " << av << "^" << aexp + << ", model sign = " << sgn << std::endl; + if (sgn == 0) { + if (d_mv[1][oa].getConst<Rational>().sgn() != 0) { + Node lemma = av.eqNode(d_zero).impNode(oa.eqNode(d_zero)); + lem.push_back(lemma); + } + return 0; + } else { + if (aexp % 2 == 0) { + exp.push_back(av.eqNode(d_zero).negate()); + return compareSign(oa, a, a_index + 1, status, exp, lem); + } else { + exp.push_back(NodeManager::currentNM()->mkNode( + sgn == 1 ? kind::GT : kind::LT, av, d_zero)); + return compareSign(oa, a, a_index + 1, status * sgn, exp, lem); + } + } + } +} + +bool NonlinearExtension::compareMonomial( + Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b, + NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem, + std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers) { + Trace("nl-alg-comp-debug") + << "Check |" << a << "| >= |" << b << "|" << std::endl; + unsigned pexp_size = exp.size(); + if (compareMonomial(oa, a, 0, a_exp_proc, ob, b, 0, b_exp_proc, 0, exp, lem, + cmp_infers)) { + return true; + } else { + exp.resize(pexp_size); + Trace("nl-alg-comp-debug") + << "Check |" << b << "| >= |" << a << "|" << std::endl; + if (compareMonomial(ob, b, 0, b_exp_proc, oa, a, 0, a_exp_proc, 0, exp, lem, + cmp_infers)) { + return true; + } else { + return false; + } + } +} + +bool NonlinearExtension::cmp_holds( + Node x, Node y, std::map<Node, std::map<Node, Node> >& cmp_infers, + std::vector<Node>& exp, std::map<Node, bool>& visited) { + if (x == y) { + return true; + } else if (visited.find(x) == visited.end()) { + visited[x] = true; + std::map<Node, std::map<Node, Node> >::iterator it = cmp_infers.find(x); + if (it != cmp_infers.end()) { + for (std::map<Node, Node>::iterator itc = it->second.begin(); + itc != it->second.end(); ++itc) { + exp.push_back(itc->second); + if (cmp_holds(itc->first, y, cmp_infers, exp, visited)) { + return true; + } + exp.pop_back(); + } + } + } + return false; +} + +// trying to show a ( >, = ) b by inequalities between variables in +// monomials a,b +bool NonlinearExtension::compareMonomial( + Node oa, Node a, unsigned a_index, NodeMultiset& a_exp_proc, Node ob, + Node b, unsigned b_index, NodeMultiset& b_exp_proc, int status, + std::vector<Node>& exp, std::vector<Node>& lem, + std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers) { + Trace("nl-alg-comp-debug") + << "compareMonomial " << oa << " and " << ob << ", indices = " << a_index + << " " << b_index << std::endl; + Assert(status == 0 || status == 2); + if (a_index == d_m_vlist[a].size() && b_index == d_m_vlist[b].size()) { + // finished, compare abstract values + int modelStatus = compare(oa, ob, 3) * -2; + Trace("nl-alg-comp") << "...finished comparison with " << oa << " <" + << status << "> " << ob + << ", model status = " << modelStatus << std::endl; + if (status != modelStatus) { + Trace("nl-alg-comp-infer") + << "infer : " << oa << " <" << status << "> " << ob << std::endl; + if (status == 2) { + // must state that all variables are non-zero + for (unsigned j = 0; j < d_m_vlist[a].size(); j++) { + exp.push_back(d_m_vlist[a][j].eqNode(d_zero).negate()); + } + } + Node clem = NodeManager::currentNM()->mkNode( + kind::IMPLIES, safeConstructNary(kind::AND, exp), + mkLit(oa, ob, status, 1)); + Trace("nl-alg-comp-lemma") << "comparison lemma : " << clem << std::endl; + lem.push_back(clem); + cmp_infers[status][oa][ob] = clem; + } + return true; + } else { + // get a/b variable information + Node av; + unsigned aexp = 0; + unsigned avo = 0; + if (a_index < d_m_vlist[a].size()) { + av = d_m_vlist[a][a_index]; + Assert(a_exp_proc[av] <= d_m_exp[a][av]); + aexp = d_m_exp[a][av] - a_exp_proc[av]; + if (aexp == 0) { + return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index, + b_exp_proc, status, exp, lem, cmp_infers); + } + Assert(d_order_vars[1].find(av) != d_order_vars[1].end()); + avo = d_order_vars[1][av]; + } + Node bv; + unsigned bexp = 0; + unsigned bvo = 0; + if (b_index < d_m_vlist[b].size()) { + bv = d_m_vlist[b][b_index]; + Assert(b_exp_proc[bv] <= d_m_exp[b][bv]); + bexp = d_m_exp[b][bv] - b_exp_proc[bv]; + if (bexp == 0) { + return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1, + b_exp_proc, status, exp, lem, cmp_infers); + } + Assert(d_order_vars[1].find(bv) != d_order_vars[1].end()); + bvo = d_order_vars[1][bv]; + } + // get "one" information + Assert(d_order_vars[1].find(d_one) != d_order_vars[1].end()); + unsigned ovo = d_order_vars[1][d_one]; + Trace("nl-alg-comp-debug") << "....vars : " << av << "^" << aexp << " " + << bv << "^" << bexp << std::endl; + + //--- cases + if (av.isNull()) { + if (bvo <= ovo) { + Trace("nl-alg-comp-debug") << "...take leading " << bv << std::endl; + // can multiply b by <=1 + exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, 1)); + return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1, + b_exp_proc, bvo == ovo ? status : 2, exp, lem, + cmp_infers); + } else { + Trace("nl-alg-comp-debug") + << "...failure, unmatched |b|>1 component." << std::endl; + return false; + } + } else if (bv.isNull()) { + if (avo >= ovo) { + Trace("nl-alg-comp-debug") << "...take leading " << av << std::endl; + // can multiply a by >=1 + exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, 1)); + return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index, + b_exp_proc, avo == ovo ? status : 2, exp, lem, + cmp_infers); + } else { + Trace("nl-alg-comp-debug") + << "...failure, unmatched |a|<1 component." << std::endl; + return false; + } + } else { + Assert(!av.isNull() && !bv.isNull()); + if (avo >= bvo) { + if (bvo < ovo && avo >= ovo) { + Trace("nl-alg-comp-debug") << "...take leading " << av << std::endl; + // do avo>=1 instead + exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, 1)); + return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index, + b_exp_proc, avo == ovo ? status : 2, exp, lem, + cmp_infers); + } else { + unsigned min_exp = aexp > bexp ? bexp : aexp; + a_exp_proc[av] += min_exp; + b_exp_proc[bv] += min_exp; + Trace("nl-alg-comp-debug") + << "...take leading " << min_exp << " from " << av << " and " + << bv << std::endl; + exp.push_back(mkLit(av, bv, avo == bvo ? 0 : 2, 1)); + bool ret = compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index, + b_exp_proc, avo == bvo ? status : 2, exp, + lem, cmp_infers); + a_exp_proc[av] -= min_exp; + b_exp_proc[bv] -= min_exp; + return ret; + } + } else { + if (bvo <= ovo) { + Trace("nl-alg-comp-debug") << "...take leading " << bv << std::endl; + // try multiply b <= 1 + exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, 1)); + return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1, + b_exp_proc, bvo == ovo ? status : 2, exp, lem, + cmp_infers); + } else { + Trace("nl-alg-comp-debug") + << "...failure, leading |b|>|a|>1 component." << std::endl; + return false; + } + } + } + } +} + +// status 0 : n equal, -1 : n superset, 1 : n subset +void NonlinearExtension::MonomialIndex::addTerm(Node n, + const std::vector<Node>& reps, + NonlinearExtension* nla, + int status, unsigned argIndex) { + if (status == 0) { + if (argIndex == reps.size()) { + d_monos.push_back(n); + } else { + d_data[reps[argIndex]].addTerm(n, reps, nla, status, argIndex + 1); + } + } + for (std::map<Node, MonomialIndex>::iterator it = d_data.begin(); + it != d_data.end(); ++it) { + if (status != 0 || argIndex == reps.size() || it->first != reps[argIndex]) { + // if we do not contain this variable, then if we were a superset, + // fail (-2), otherwise we are subset. if we do contain this + // variable, then if we were equal, we are superset since variables + // are ordered, otherwise we remain the same. + int new_status = + std::find(reps.begin(), reps.end(), it->first) == reps.end() + ? (status >= 0 ? 1 : -2) + : (status == 0 ? -1 : status); + if (new_status != -2) { + it->second.addTerm(n, reps, nla, new_status, argIndex); + } + } + } + // compare for subsets + for (unsigned i = 0; i < d_monos.size(); i++) { + Node m = d_monos[i]; + if (m != n) { + // we are superset if we are equal and haven't traversed all variables + int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status; + Trace("nl-alg-mindex-debug") << " compare " << n << " and " << m + << ", status = " << cstatus << std::endl; + if (cstatus <= 0 && nla->isMonomialSubset(m, n)) { + nla->registerMonomialSubset(m, n); + Trace("nl-alg-mindex-debug") << "...success" << std::endl; + } else if (cstatus >= 0 && nla->isMonomialSubset(n, m)) { + nla->registerMonomialSubset(n, m); + Trace("nl-alg-mindex-debug") << "...success (rev)" << std::endl; + } + } + } +} + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h new file mode 100644 index 000000000..7c7bfbce9 --- /dev/null +++ b/src/theory/arith/nonlinear_extension.h @@ -0,0 +1,208 @@ +/********************* */ +/*! \file nonlinear_extension.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Extensions for incomplete handling of nonlinear multiplication. + ** + ** Extensions to the theory of arithmetic incomplete handling of nonlinear + ** multiplication via axiom instantiations. + **/ + +#ifndef __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H +#define __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H + +#include <stdint.h> + +#include <map> +#include <queue> +#include <set> +#include <utility> +#include <vector> + +#include "context/cdhashset.h" +#include "context/cdinsert_hashmap.h" +#include "context/cdlist.h" +#include "context/cdqueue.h" +#include "context/context.h" +#include "expr/kind.h" +#include "expr/node.h" +#include "theory/arith/theory_arith.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +typedef std::map<Node, unsigned> NodeMultiset; + +class NonlinearExtension { + public: + NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee); + ~NonlinearExtension(); + bool getCurrentSubstitution(int effort, const std::vector<Node>& vars, + std::vector<Node>& subs, + std::map<Node, std::vector<Node> >& exp); + + std::pair<bool, Node> isExtfReduced(int effort, Node n, Node on, + const std::vector<Node>& exp) const; + void check(Theory::Effort e); + bool needsCheckLastEffort() const { return d_needsLastCall; } + int compare(Node i, Node j, unsigned orderType) const; + int compare_value(Node i, Node j, unsigned orderType) const; + + bool isMonomialSubset(Node a, Node b) const; + void registerMonomialSubset(Node a, Node b); + + private: + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + + // monomial information (context-independent) + class MonomialIndex { + public: + // status 0 : n equal, -1 : n superset, 1 : n subset + void addTerm(Node n, const std::vector<Node>& reps, NonlinearExtension* nla, + int status = 0, unsigned argIndex = 0); + + private: + std::map<Node, MonomialIndex> d_data; + std::vector<Node> d_monos; + }; /* class MonomialIndex */ + + // constraint information (context-independent) + struct ConstraintInfo { + public: + Node d_rhs; + Node d_coeff; + Kind d_type; + }; /* struct ConstraintInfo */ + + // Check assertions for consistency in the effort LAST_CALL with a subset of + // the assertions, false_asserts, evaluate to false in the current model. + void checkLastCall(const std::vector<Node>& assertions, + const std::set<Node>& false_asserts); + + // Returns a vector containing a split on whether each term is 0 or not for + // those terms that have not been split on in the current context. + std::vector<Node> splitOnZeros(const std::vector<Node>& terms); + + static bool isArithKind(Kind k); + static Node mkLit(Node a, Node b, int status, int orderType = 0); + static Node mkAbs(Node a); + static Kind joinKinds(Kind k1, Kind k2); + static Kind transKinds(Kind k1, Kind k2); + Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const; + + // register monomial + void registerMonomial(Node n); + void setMonomialFactor(Node a, Node b, const NodeMultiset& common); + + void registerConstraint(Node atom); + // index = 0 : concrete, 1 : abstract + Node computeModelValue(Node n, unsigned index = 0); + + Node get_compare_value(Node i, unsigned orderType) const; + void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order, + unsigned orderType); + + // Returns the subset of assertions that evaluate to false in the model. + std::set<Node> getFalseInModel(const std::vector<Node>& assertions); + + // status + // 0 : equal + // 1 : greater than or equal + // 2 : greater than + // -X : (less) + // in these functions we are iterating over variables of monomials + // initially : exp => ( oa = a ^ ob = b ) + int compareSign(Node oa, Node a, unsigned a_index, int status, + std::vector<Node>& exp, std::vector<Node>& lem); + bool compareMonomial( + Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b, + NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem, + std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers); + bool compareMonomial( + Node oa, Node a, unsigned a_index, NodeMultiset& a_exp_proc, Node ob, + Node b, unsigned b_index, NodeMultiset& b_exp_proc, int status, + std::vector<Node>& exp, std::vector<Node>& lem, + std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers); + bool cmp_holds(Node x, Node y, + std::map<Node, std::map<Node, Node> >& cmp_infers, + std::vector<Node>& exp, std::map<Node, bool>& visited); + + bool isEntailed(Node n, bool pol); + + // Potentially sends lem on the output channel if lem has not been sent on the + // output channel in this context. Returns the number of lemmas sent on the + // output channel. + int flushLemma(Node lem); + + // Potentially sends lemmas to the output channel and clears lemmas. Returns + // the number of lemmas sent to the output channel. + int flushLemmas(std::vector<Node>& lemmas); + + // Returns the NodeMultiset for an existing monomial. + const NodeMultiset& getMonomialExponentMap(Node monomial) const; + + // Map from monomials to var^index. + typedef std::map<Node, NodeMultiset> MonomialExponentMap; + MonomialExponentMap d_m_exp; + + std::map<Node, std::vector<Node> > d_m_vlist; + NodeMultiset d_m_degree; + // monomial index, by sorted variables + MonomialIndex d_m_index; + // list of all monomials + std::vector<Node> d_monomials; + // containment ordering + std::map<Node, std::vector<Node> > d_m_contain_children; + std::map<Node, std::vector<Node> > d_m_contain_parent; + std::map<Node, std::map<Node, Node> > d_m_contain_mult; + std::map<Node, std::map<Node, Node> > d_m_contain_umult; + // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors + std::map<Node, std::map<Node, Node> > d_mono_diff; + + // cache of all lemmas sent + NodeSet d_lemmas; + NodeSet d_zero_split; + + // utilities + Node d_zero; + Node d_one; + Node d_neg_one; + Node d_true; + Node d_false; + + // The theory of arithmetic containing this extension. + TheoryArith& d_containing; + + // pointer to used equality engine + eq::EqualityEngine* d_ee; + // needs last call effort + bool d_needsLastCall; + + // if d_c_info[lit][x] = ( r, coeff, k ), then ( lit <=> (coeff * x) <k> r ) + std::map<Node, std::map<Node, ConstraintInfo> > d_c_info; + std::map<Node, std::map<Node, bool> > d_c_info_maxm; + std::vector<Node> d_constraints; + + // model values/orderings + // model values + std::map<Node, Node> d_mv[2]; + + // ordering, stores variables and 0,1,-1 + std::map<unsigned, NodeMultiset> d_order_vars; + std::vector<Node> d_order_points; +}; /* class NonlinearExtension */ + +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index ec396b24e..f8de2f239 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -103,7 +103,7 @@ bool VarList::isMember(Node n) { if(Variable::isMember(n)) { return true; } - if(n.getKind() == kind::MULT) { + if(n.getKind() == kind::NONLINEAR_MULT) { Node::iterator curr = n.begin(), end = n.end(); Node prev = *curr; if(!Variable::isMember(prev)) return false; @@ -189,7 +189,7 @@ VarList VarList::operator*(const VarList& other) const { merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result, cmp); Assert(result.size() >= 2); - Node mult = NodeManager::currentNM()->mkNode(kind::MULT, result); + Node mult = NodeManager::currentNM()->mkNode(kind::NONLINEAR_MULT, result); return VarList::parseVarList(mult); } } diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index d57d781f1..d0c9df1a6 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -487,7 +487,7 @@ private: static Node multList(const std::vector<Variable>& list) { Assert(list.size() >= 2); - return makeNode(kind::MULT, list.begin(), list.end()); + return makeNode(kind::NONLINEAR_MULT, list.begin(), list.end()); } VarList() : NodeWrapper(Node::null()) {} @@ -589,7 +589,7 @@ public: bool empty() const { return getNode().isNull(); } bool singleton() const { - return !empty() && getNode().getKind() != kind::MULT; + return !empty() && getNode().getKind() != kind::NONLINEAR_MULT; } int size() const { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9627b9a1a..5af613a94 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -37,6 +37,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, , d_ppRewriteTimer("theory::arith::ppRewriteTimer") { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); + if (options::nlAlg()) { + setupExtTheory(); + getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT); + } } TheoryArith::~TheoryArith(){ @@ -56,11 +60,6 @@ void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_internal->setMasterEqualityEngine(eq); } -void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) { - this->Theory::setQuantifiersEngine(qe); - d_internal->setQuantifiersEngine(qe); -} - void TheoryArith::addSharedTerm(TNode n){ d_internal->addSharedTerm(n); } @@ -83,10 +82,22 @@ void TheoryArith::check(Effort effortLevel){ d_internal->check(effortLevel); } +bool TheoryArith::needsCheckLastEffort() { + return d_internal->needsCheckLastEffort(); +} + Node TheoryArith::explain(TNode n) { return d_internal->explain(n); } +bool TheoryArith::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { + return d_internal->getCurrentSubstitution( effort, vars, subs, exp ); +} + +bool TheoryArith::isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ) { + return d_internal->isExtfReduced( effort, n, on, exp ); +} + void TheoryArith::propagate(Effort e) { d_internal->propagate(e); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 51bbd67f3..267c10e4b 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -53,11 +53,13 @@ public: Node expandDefinition(LogicRequest &logicRequest, Node node); void setMasterEqualityEngine(eq::EqualityEngine* eq); - void setQuantifiersEngine(QuantifiersEngine* qe); void check(Effort e); + bool needsCheckLastEffort(); void propagate(Effort e); Node explain(TNode n); + bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); + bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ); void collectModelInfo( TheoryModel* m, bool fullModel ); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 069d3530c..ba48f1704 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -61,6 +61,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" +#include "theory/arith/nonlinear_extension.h" #include "theory/ite_utilities.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/rewriter.h" @@ -79,6 +80,23 @@ namespace CVC4 { namespace theory { namespace arith { +namespace attr { + struct ToIntegerTag { }; + struct LinearIntDivTag { }; +}/* CVC4::theory::arith::attr namespace */ + +/** + * This attribute maps the child of a to_int / is_int to the + * corresponding integer skolem. + */ +typedef expr::CDAttribute<attr::ToIntegerTag, Node> ToIntegerAttr; + +/** + * This attribute maps division-by-constant-k terms to a variable + * used to eliminate them. + */ +typedef expr::CDAttribute<attr::LinearIntDivTag, Node> LinearIntDivAttr; + static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum); static double fRand(double fMin, double fMax); static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap); @@ -93,7 +111,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), d_learner(u), - d_quantEngine(NULL), d_assertionsThatDoNotMatchTheirLiterals(c), d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), @@ -118,7 +135,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), - + d_nonlinearExtension( NULL ), d_pass1SDP(NULL), d_otherSDP(NULL), d_lastContextIntegerAttempted(c,-1), @@ -144,11 +161,17 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_statistics() { srand(79); + + if( options::nlAlg() ){ + d_nonlinearExtension = new NonlinearExtension( + containing, d_congruenceManager.getEqualityEngine()); + } } TheoryArithPrivate::~TheoryArithPrivate(){ if(d_treeLog != NULL){ delete d_treeLog; } if(d_approxStats != NULL) { delete d_approxStats; } + if(d_nonlinearExtension != NULL) { delete d_nonlinearExtension; } } static bool contains(const ConstraintCPVec& v, ConstraintP con){ @@ -205,12 +228,217 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& // return safeConstructNary(nb); } -void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_congruenceManager.setMasterEqualityEngine(eq); +// Returns a skolem variable that is constrained to equal +// division_total(num, den) in the current context. May add lemmas to out. +static Node getSkolemConstrainedToDivisionTotal( + Node num, Node den, OutputChannel* out) { + NodeManager* nm = NodeManager::currentNM(); + Node total_div_node = nm->mkNode(kind::DIVISION_TOTAL, num, den); + Node total_div_skolem; + if(total_div_node.getAttribute(LinearIntDivAttr(), total_div_skolem)) { + return total_div_skolem; + } + total_div_skolem = nm->mkSkolem("DivisionTotalSkolem", nm->integerType(), + "the result of an intdiv-by-k term"); + total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem); + Node zero = mkRationalNode(0); + Node lemma = den.eqNode(zero).iteNode( + total_div_skolem.eqNode(zero), num.eqNode(mkMult(total_div_skolem, den))); + out->lemma(lemma); + return total_div_skolem; +} + +// Returns a skolem variable that is constrained to equal division(num, den) in +// the current context. May add lemmas to out. +static Node getSkolemConstrainedToDivision( + Node num, Node den, Node div0Func, OutputChannel* out) { + NodeManager* nm = NodeManager::currentNM(); + Node div_node = nm->mkNode(kind::DIVISION, num, den); + Node div_skolem; + if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) { + return div_skolem; + } + div_skolem = nm->mkSkolem("DivisionSkolem", nm->integerType(), + "the result of an intdiv-by-k term"); + div_node.setAttribute(LinearIntDivAttr(), div_skolem); + Node div0 = nm->mkNode(APPLY_UF, div0Func, num); + Node total_div = getSkolemConstrainedToDivisionTotal(num, den, out); + out->lemma(mkOnZeroIte(den, div_skolem, div0, total_div)); + return div_skolem; +} + + +// Integer division axioms: +// These concenrate the high level constructs needed to constrain the functions: +// div, mod, div_total and mod_total. +// +// The high level constraint. +// (for all ((m Int) (n Int)) +// (=> (distinct n 0) +// (let ((q (div m n)) (r (mod m n))) +// (and (= m (+ (* n q) r)) +// (<= 0 r (- (abs n) 1)))))) +// +// We now add division by 0 functions. +// (for all ((m Int) (n Int)) +// (let ((q (div m n)) (r (mod m n))) +// (ite (= n 0) +// (and (= q (div_0_func m)) (= r (mod_0_func m))) +// (and (= m (+ (* n q) r)) +// (<= 0 r (- (abs n) 1))))))) +// +// We now express div and mod in terms of div_total and mod_total. +// (for all ((m Int) (n Int)) +// (let ((q (div m n)) (r (mod m n))) +// (ite (= n 0) +// (and (= q (div_0_func m)) (= r (mod_0_func m))) +// (and (= q (div_total m n)) (= r (mod_total m n)))))) +// +// Alternative div_total and mod_total without the abs function: +// (for all ((m Int) (n Int)) +// (let ((q (div_total m n)) (r (mod_total m n))) +// (ite (= n 0) +// (and (= q 0) (= r 0)) +// (and (r = m - n * q) +// (ite (> n 0) +// (n*q <= m < n*q + n) +// (n*q <= m < n*q - n)))))) + + +// Returns a formula that entails that q equals the total integer division of m +// by n. +// (for all ((m Int) (n Int)) +// (let ((q (div_total m n))) +// (ite (= n 0) +// (= q 0) +// (ite (> n 0) +// (n*q <= m < n*q + n) +// (n*q <= m < n*q - n))))) +Node mkAxiomForTotalIntDivision(Node m, Node n, Node q) { + NodeManager* nm = NodeManager::currentNM(); + Node zero = mkRationalNode(0); + // (n*q <= m < n*q + n) is equivalent to (0 <= m - n*q < n). + Node diff = nm->mkNode(kind::MINUS, m, mkMult(n, q)); + Node when_n_is_positive = mkInRange(diff, zero, n); + Node when_n_is_negative = mkInRange(diff, zero, nm->mkNode(kind::UMINUS, n)); + return n.eqNode(zero).iteNode( + q.eqNode(zero), nm->mkNode(kind::GT, n, zero) + .iteNode(when_n_is_positive, when_n_is_negative)); +} + +// Returns a formula that entails that r equals the integer division total of m +// by n assuming q is equal to (div_total m n). +// (for all ((m Int) (n Int)) +// (let ((q (div_total m n)) (r (mod_total m n))) +// (ite (= n 0) +// (= r 0) +// (= r (- m (n * q)))))) +Node mkAxiomForTotalIntMod(Node m, Node n, Node q, Node r) { + NodeManager* nm = NodeManager::currentNM(); + Node diff = nm->mkNode(kind::MINUS, m, mkMult(n, q)); + return mkOnZeroIte(n, r, mkRationalNode(0), diff); +} + +// Returns an expression that constrains a term to be the result of the +// [total] integer division of num by den. Equivalently: +// (and (=> (den > 0) (den*term <= num < den*term + den)) +// (=> (den < 0) (den*term <= num < den*term - den)) +// (=> (den = 0) (term = 0))) +// static Node mkIntegerDivisionConstraint(Node term, Node num, Node den) { +// // We actually encode: +// // (and (=> (den > 0) (0 <= num - den*term < den)) +// // (=> (den < 0) (0 <= num - den*term < -den)) +// // (=> (den = 0) (term = 0))) +// NodeManager* nm = NodeManager::currentNM(); +// Node zero = nm->mkConst(Rational(0)); +// Node den_is_positive = nm->mkNode(kind::GT, den, zero); +// Node den_is_negative = nm->mkNode(kind::LT, den, zero); +// Node diff = nm->mkNode(kind::MINUS, num, mkMult(den, term)); +// Node when_den_positive = den_positive.impNode(mkInRange(diff, zero, den)); +// Node when_den_negative = den_negative.impNode( +// mkInRange(diff, zero, nm->mkNode(kind::UMINUS, den))); +// Node when_den_is_zero = (den.eqNode(zero)).impNode(term.eqNode(zero)); +// return mk->mkNode(kind::AND, when_den_positive, when_den_negative, +// when_den_is_zero); +// } + +// Returns a skolem variable that is constrained to equal +// integer_division_total(num, den) in the current context. May add lemmas to +// out. +static Node getSkolemConstrainedToIntegerDivisionTotal( + Node num, Node den, OutputChannel* out) { + NodeManager* nm = NodeManager::currentNM(); + Node total_div_node = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); + Node total_div_skolem; + if(total_div_node.getAttribute(LinearIntDivAttr(), total_div_skolem)) { + return total_div_skolem; + } + total_div_skolem = nm->mkSkolem("linearIntDiv", nm->integerType(), + "the result of an intdiv-by-k term"); + total_div_node.setAttribute(LinearIntDivAttr(), total_div_skolem); + out->lemma(mkAxiomForTotalIntDivision(num, den, total_div_skolem)); + return total_div_skolem; +} + +// Returns a skolem variable that is constrained to equal +// integer_division(num, den) in the current context. May add lemmas to out. +static Node getSkolemConstrainedToIntegerDivision( + Node num, Node den, Node div0Func, OutputChannel* out) { + NodeManager* nm = NodeManager::currentNM(); + Node div_node = nm->mkNode(kind::INTS_DIVISION, num, den); + Node div_skolem; + if(div_node.getAttribute(LinearIntDivAttr(), div_skolem)) { + return div_skolem; + } + div_skolem = nm->mkSkolem("IntDivSkolem", nm->integerType(), + "the result of an intdiv-by-k term"); + div_node.setAttribute(LinearIntDivAttr(), div_skolem); + Node div0 = nm->mkNode(APPLY_UF, div0Func, num); + Node total_div = getSkolemConstrainedToIntegerDivisionTotal(num, den, out); + out->lemma(mkOnZeroIte(den, div_skolem, div0, total_div)); + return div_skolem; +} + +// Returns a skolem variable that is constrained to equal +// integer_modulus_total(num, den) in the current context. May add lemmas to +// out. +static Node getSkolemConstrainedToIntegerModulusTotal( + Node num, Node den, OutputChannel* out) { + NodeManager* nm = NodeManager::currentNM(); + Node total_mod_node = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); + Node total_mod_skolem; + if(total_mod_node.getAttribute(LinearIntDivAttr(), total_mod_skolem)) { + return total_mod_skolem; + } + total_mod_skolem = nm->mkSkolem("IntModTotalSkolem", nm->integerType(), + "the result of an intdiv-by-k term"); + total_mod_node.setAttribute(LinearIntDivAttr(), total_mod_skolem); + Node total_div = getSkolemConstrainedToIntegerDivisionTotal(num, den, out); + out->lemma(mkAxiomForTotalIntMod(num, den, total_div, total_mod_skolem)); + return total_mod_skolem; +} + +// Returns a skolem variable that is constrained to equal +// integer_modulus(num, den) in the current context. May add lemmas to out. +static Node getSkolemConstrainedToIntegerModulus( + Node num, Node den, Node mod0Func, OutputChannel* out) { + NodeManager* nm = NodeManager::currentNM(); + Node mod_node = nm->mkNode(kind::INTS_MODULUS, num, den); + Node mod_skolem; + if(mod_node.getAttribute(LinearIntDivAttr(), mod_skolem)) { + return mod_skolem; + } + mod_skolem = nm->mkSkolem("IntModSkolem", nm->integerType(), + "the result of an intdiv-by-k term"); + mod_node.setAttribute(LinearIntDivAttr(), mod_skolem); + Node mod0 = nm->mkNode(APPLY_UF, mod0Func, num); + Node total_mod = getSkolemConstrainedToIntegerModulusTotal(num, den, out); + out->lemma(mkOnZeroIte(den, mod_skolem, mod0, total_mod)); + return mod_skolem; } -void TheoryArithPrivate::setQuantifiersEngine(QuantifiersEngine* qe) { - d_quantEngine = qe; +void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_congruenceManager.setMasterEqualityEngine(eq); } Node TheoryArithPrivate::getRealDivideBy0Func(){ @@ -1097,23 +1325,6 @@ Node TheoryArithPrivate::getModelValue(TNode term) { } } -namespace attr { - struct ToIntegerTag { }; - struct LinearIntDivTag { }; -}/* CVC4::theory::arith::attr namespace */ - -/** - * This attribute maps the child of a to_int / is_int to the - * corresponding integer skolem. - */ -typedef expr::CDAttribute<attr::ToIntegerTag, Node> ToIntegerAttr; - -/** - * This attribute maps division-by-constant-k terms to a variable - * used to eliminate them. - */ -typedef expr::CDAttribute<attr::LinearIntDivTag, Node> LinearIntDivAttr; - Node TheoryArithPrivate::ppRewriteTerms(TNode n) { if(Theory::theoryOf(n) != THEORY_ARITH) { return n; @@ -1125,81 +1336,62 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { case kind::TO_INTEGER: case kind::IS_INTEGER: { - Node intVar; - if(!n[0].getAttribute(ToIntegerAttr(), intVar)) { - intVar = nm->mkSkolem("toInt", nm->integerType(), "a conversion of a Real term to its Integer part"); - n[0].setAttribute(ToIntegerAttr(), intVar); - d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LT, nm->mkNode(kind::MINUS, n[0], nm->mkConst(Rational(1))), intVar), nm->mkNode(kind::LEQ, intVar, n[0]))); - } - if(n.getKind() == kind::TO_INTEGER) { - Node node = intVar; - return node; - } else { - Node node = nm->mkNode(kind::EQUAL, n[0], intVar); - return node; - } - Unreachable(); + Node toIntSkolem; + if(!n[0].getAttribute(ToIntegerAttr(), toIntSkolem)) { + toIntSkolem = nm->mkSkolem("toInt", nm->integerType(), + "a conversion of a Real term to its Integer part"); + n[0].setAttribute(ToIntegerAttr(), toIntSkolem); + // n[0] - 1 < toIntSkolem <= n[0] + // -1 < toIntSkolem - n[0] <= 0 + // 0 <= n[0] - toIntSkolem < 1 + Node one = mkRationalNode(1); + Node lem = mkAxiomForTotalIntDivision(n[0], one, toIntSkolem); + d_containing.d_out->lemma(lem); + } + if(k == kind::IS_INTEGER) { + return nm->mkNode(kind::EQUAL, n[0], toIntSkolem); + } + Assert(k == kind::TO_INTEGER); + return toIntSkolem; } - + case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: case kind::INTS_DIVISION: case kind::INTS_DIVISION_TOTAL: { - if(!options::rewriteDivk()) { - return n; - } - Node num = Rewriter::rewrite(n[0]); Node den = Rewriter::rewrite(n[1]); - if(den.isConst()) { - const Rational& rat = den.getConst<Rational>(); - Assert(!num.isConst()); - if(rat != 0) { - Node intVar; - Node rw = nm->mkNode(k, num, den); - if(!rw.getAttribute(LinearIntDivAttr(), intVar)) { - intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term"); - rw.setAttribute(LinearIntDivAttr(), intVar); - if(rat > 0) { - d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1))))))); - } else { - d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1))))))); - } - } - return intVar; - } - } - break; - } - - case kind::INTS_MODULUS: - case kind::INTS_MODULUS_TOTAL: { - if(!options::rewriteDivk()) { + if (!options::rewriteDivk() && den.isConst()) { return n; } Node num = Rewriter::rewrite(n[0]); + if (k == kind::INTS_MODULUS) { + return getSkolemConstrainedToIntegerModulus( + num, den, getIntModulusBy0Func(), d_containing.d_out); + } else if (k == kind::INTS_MODULUS_TOTAL) { + return getSkolemConstrainedToIntegerModulusTotal(num, den, + d_containing.d_out); + } else if (k == kind::INTS_DIVISION) { + return getSkolemConstrainedToIntegerDivision( + num, den, getIntDivideBy0Func(), d_containing.d_out); + } + Assert(k == kind::INTS_DIVISION_TOTAL); + return getSkolemConstrainedToIntegerDivisionTotal(num, den, + d_containing.d_out); + } + case kind::DIVISION: + case kind::DIVISION_TOTAL: { + Node num = Rewriter::rewrite(n[0]); Node den = Rewriter::rewrite(n[1]); - if(den.isConst()) { - const Rational& rat = den.getConst<Rational>(); - Assert(!num.isConst()); - if(rat != 0) { - Node intVar; - Node rw = nm->mkNode(k, num, den); - if(!rw.getAttribute(LinearIntDivAttr(), intVar)) { - intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term"); - rw.setAttribute(LinearIntDivAttr(), intVar); - if(rat > 0) { - d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1))))))); - } else { - d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1))))))); - } - } - Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar)); - return node; - } + Assert(!den.isConst()); + if (k == kind::DIVISION) { + return getSkolemConstrainedToDivision(num, den, getRealDivideBy0Func(), + d_containing.d_out); } - break; + Assert(k == kind::DIVISION_TOTAL); + return getSkolemConstrainedToDivisionTotal(num, den, d_containing.d_out); } default: - ; + break; } for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) { @@ -1382,8 +1574,10 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic."); } - setIncomplete(); - d_nlIncomplete = true; + if( !options::nlAlg() ){ + setIncomplete(); + d_nlIncomplete = true; + } ++(d_statistics.d_statUserVariables); requestArithVar(vlNode, false, false); @@ -1460,7 +1654,7 @@ Node TheoryArithPrivate::definingIteForDivLike(Node divLike){ // (DIVISION n d) // (ite (= d 0) // (APPLY [div_0_skolem_function] n) - // (DIVISION_TOTAL x y)))) + // (DIVISION_TOTAL n d)))) Polynomial n = Polynomial::parsePolynomial(divLike[0]); Polynomial d = Polynomial::parsePolynomial(divLike[1]); @@ -1512,19 +1706,7 @@ Node TheoryArithPrivate::axiomIteForTotalIntDivision(Node int_div_like){ Kind k = int_div_like.getKind(); Assert(k == INTS_DIVISION_TOTAL || k == INTS_MODULUS_TOTAL); - // (for all ((m Int) (n Int)) - // (=> (distinct n 0) - // (let ((q (div m n)) (r (mod m n))) - // (and (= m (+ (* n q) r)) - // (<= 0 r (- (abs n) 1)))))) - - // Updated for div 0 functions - // (for all ((m Int) (n Int)) - // (let ((q (div m n)) (r (mod m n))) - // (ite (= n 0) - // (and (= q (div_0_func m)) (= r (mod_0_func m))) - // (and (= m (+ (* n q) r)) - // (<= 0 r (- (abs n) 1))))))) + // See the discussion of integer division axioms above. Polynomial n = Polynomial::parsePolynomial(int_div_like[0]); Polynomial d = Polynomial::parsePolynomial(int_div_like[1]); @@ -1637,6 +1819,10 @@ void TheoryArithPrivate::setupAtom(TNode atom) { void TheoryArithPrivate::preRegisterTerm(TNode n) { Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; + + if( options::nlAlg() ){ + d_containing.getExtTheory()->registerTermRec( n ); + } try { if(isRelationOperator(n.getKind())){ @@ -3456,7 +3642,14 @@ bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{ void TheoryArithPrivate::check(Theory::Effort effortLevel){ Assert(d_currentPropagationList.empty()); - if(done() && !Theory::fullEffort(effortLevel) && ( d_qflraStatus == Result::SAT) ){ + if(done() && effortLevel < Theory::EFFORT_FULL && ( d_qflraStatus == Result::SAT) ){ + return; + } + + if(effortLevel == Theory::EFFORT_LAST_CALL){ + if( options::nlAlg() ){ + d_nonlinearExtension->check( effortLevel ); + } return; } @@ -3772,6 +3965,13 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ } } }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel() + + if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){ + if( options::nlAlg() ){ + d_nonlinearExtension->check( effortLevel ); + } + } + if(Theory::fullEffort(effortLevel) && d_nlIncomplete){ // TODO this is total paranoia setIncomplete(); @@ -3947,7 +4147,13 @@ void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{ } } - +bool TheoryArithPrivate::needsCheckLastEffort() { + if( options::nlAlg() ){ + return d_nonlinearExtension->needsCheckLastEffort(); + }else{ + return false; + } +} Node TheoryArithPrivate::explain(TNode n) { @@ -3978,6 +4184,28 @@ Node TheoryArithPrivate::explain(TNode n) { } } +bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { + if( options::nlAlg() ){ + return d_nonlinearExtension->getCurrentSubstitution( effort, vars, subs, exp ); + }else{ + return false; + } +} + +bool TheoryArithPrivate::isExtfReduced(int effort, Node n, Node on, + std::vector<Node>& exp) { + if (options::nlAlg()) { + std::pair<bool, Node> reduced = + d_nonlinearExtension->isExtfReduced(effort, n, on, exp); + if (!reduced.second.isNull()) { + exp.clear(); + exp.push_back(reduced.second); + } + return reduced.first; + } else { + return false; // d_containing.isExtfReduced( effort, n, on ); + } +} void TheoryArithPrivate::propagate(Theory::Effort e) { // This uses model values for safety. Disable for now. @@ -4060,7 +4288,8 @@ DeltaRational TheoryArithPrivate::getDeltaValue(TNode n) const throw (DeltaRatio return value; } - case kind::MULT: { // 2+ args + case kind::MULT: + case kind::NONLINEAR_MULT: { // 2+ args DeltaRational value(1); unsigned variableParts = 0; for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index ed7efe008..d4afaccc6 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -83,6 +83,8 @@ namespace inferbounds { } class InferBoundsResult; +class NonlinearExtension; + /** * Implementation of QF_LRA. * Based upon: @@ -127,8 +129,6 @@ private: /** Static learner. */ ArithStaticLearner d_learner; - /** quantifiers engine */ - QuantifiersEngine * d_quantEngine; //std::vector<ArithVar> d_pool; public: void releaseArithVar(ArithVar v); @@ -373,6 +373,9 @@ private: FCSimplexDecisionProcedure d_fcSimplex; SumOfInfeasibilitiesSPD d_soiSimplex; AttemptSolutionSDP d_attemptSolSimplex; + + /** non-linear algebraic approach */ + NonlinearExtension * d_nonlinearExtension; bool solveRealRelaxation(Theory::Effort effortLevel); @@ -432,9 +435,11 @@ public: void setQuantifiersEngine(QuantifiersEngine* qe); void check(Theory::Effort e); + bool needsCheckLastEffort(); void propagate(Theory::Effort e); Node explain(TNode n); - + bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); + bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ); Rational deltaValueForTotalOrder() const; diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index b0f2efcda..de27fc834 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -66,7 +66,6 @@ void TheoryBool::check(Effort level) { // Get all the assertions Assertion assertion = get(); TNode fact = assertion.assertion; - Trace("ajr-bool") << "Assert : " << fact << std::endl; } if( Theory::fullEffort(level) ){ } diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 8fecaa78d..0ddc447be 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -136,6 +136,14 @@ Node QuantArith::mkNode( std::map< Node, Node >& msum ) { return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); } +Node QuantArith::mkCoeffTerm( Node coeff, Node t ) { + if( coeff.isNull() ){ + return t; + }else{ + return NodeManager::currentNM()->mkNode( kind::MULT, coeff, t ); + } +} + // given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where: // veq_c is either null (meaning 1), or positive. // return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed. diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index b4264135c..fcc162a7a 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -91,6 +91,7 @@ public: static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); static Node mkNode( std::map< Node, Node >& msum ); + static Node mkCoeffTerm( Node coeff, Node t ); //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ); static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 5e14d1cb5..37d65972e 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -359,9 +359,10 @@ EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { } -ExtTheory::ExtTheory( Theory * p ) : d_parent( p ), -d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), -d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_has_extf( p->getSatContext() ){ + +ExtTheory::ExtTheory( Theory * p, bool cacheEnabled ) : d_parent( p ), +d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), d_has_extf( p->getSatContext() ), +d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_cacheEnabled( cacheEnabled ){ d_true = NodeManager::currentNM()->mkConst( true ); } @@ -391,62 +392,92 @@ std::vector<Node> ExtTheory::collectVars(Node n) { return vars; } +Node ExtTheory::getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache ) { + if( useCache ){ + Assert( d_gst_cache[effort].find( term )!=d_gst_cache[effort].end() ); + exp.insert( exp.end(), d_gst_cache[effort][term].d_exp.begin(), d_gst_cache[effort][term].d_exp.end() ); + return d_gst_cache[effort][term].d_sterm; + }else{ + std::vector< Node > terms; + terms.push_back( term ); + std::vector< Node > sterms; + std::vector< std::vector< Node > > exps; + getSubstitutedTerms( effort, terms, sterms, exps, useCache ); + Assert( sterms.size()==1 ); + Assert( exps.size()==1 ); + exp.insert( exp.end(), exps[0].begin(), exps[0].end() ); + return sterms[0]; + } +} + //do inferences void ExtTheory::getSubstitutedTerms(int effort, const std::vector<Node>& terms, std::vector<Node>& sterms, - std::vector<std::vector<Node> >& exp) { - Trace("extt-debug") << "Currently " << d_ext_func_terms.size() - << " extended functions." << std::endl; - Trace("extt-debug") << "..." << terms.size() << " to reduce." << std::endl; - if( !terms.empty() ){ - //all variables we need to find a substitution for - std::vector< Node > vars; - std::vector< Node > sub; - std::map< Node, std::vector< Node > > expc; + std::vector<std::vector<Node> >& exp, + bool useCache) { + if (useCache) { for( unsigned i=0; i<terms.size(); i++ ){ - //do substitution, rewrite Node n = terms[i]; - std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); - Trace("extt-debug") << "Check extf : " << n << std::endl; - Assert( iti!=d_extf_info.end() ); - for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){ - if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){ - vars.push_back( iti->second.d_vars[i] ); - } - } + Assert( d_gst_cache[effort].find( n )!=d_gst_cache[effort].end() ); + sterms.push_back( d_gst_cache[effort][n].d_sterm ); + exp.push_back( std::vector< Node >() ); + exp[0].insert( exp[0].end(), d_gst_cache[effort][n].d_exp.begin(), d_gst_cache[effort][n].d_exp.end() ); } - //get the current substitution for all variables - if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){ - Assert( vars.size()==sub.size() ); + }else{ + Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " << d_ext_func_terms.size() << " extended functions." << std::endl; + if( !terms.empty() ){ + //all variables we need to find a substitution for + std::vector< Node > vars; + std::vector< Node > sub; + std::map< Node, std::vector< Node > > expc; + for( unsigned i=0; i<terms.size(); i++ ){ + //do substitution, rewrite + Node n = terms[i]; + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){ + if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){ + vars.push_back( iti->second.d_vars[i] ); + } + } + } + bool useSubs = d_parent->getCurrentSubstitution( effort, vars, sub, expc ); + //get the current substitution for all variables + Assert( !useSubs || vars.size()==sub.size() ); for( unsigned i=0; i<terms.size(); i++ ){ - //do substitution Node n = terms[i]; - Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() ); + Node ns = n; std::vector< Node > expn; - if( ns!=n ){ - //build explanation: explanation vars = sub for each vars in FV( n ) - std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); - Assert( iti!=d_extf_info.end() ); - for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){ - Node v = iti->second.d_vars[j]; - std::map< Node, std::vector< Node > >::iterator itx = expc.find( v ); - if( itx!=expc.end() ){ - for( unsigned k=0; k<itx->second.size(); k++ ){ - if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){ - expn.push_back( itx->second[k] ); + if( useSubs ){ + //do substitution + ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() ); + if( ns!=n ){ + //build explanation: explanation vars = sub for each vars in FV( n ) + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){ + Node v = iti->second.d_vars[j]; + std::map< Node, std::vector< Node > >::iterator itx = expc.find( v ); + if( itx!=expc.end() ){ + for( unsigned k=0; k<itx->second.size(); k++ ){ + if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){ + expn.push_back( itx->second[k] ); + } } } } } + Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl; } - Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl; //add to vector sterms.push_back( ns ); exp.push_back( expn ); - } - }else{ - for( unsigned i=0; i<terms.size(); i++ ){ - sterms.push_back( terms[i] ); + //add to cache + if( d_cacheEnabled ){ + d_gst_cache[effort][n].d_sterm = ns; + d_gst_cache[effort][n].d_exp.clear(); + d_gst_cache[effort][n].d_exp.insert( d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end() ); + } } } } @@ -469,7 +500,7 @@ bool ExtTheory::doInferencesInternal(int effort, const std::vector<Node>& terms, if( !nr.isNull() && n!=nr ){ Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ); if( sendLemma( lem, true ) ){ - Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl; + Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl; addedLemma = true; } } @@ -480,11 +511,13 @@ bool ExtTheory::doInferencesInternal(int effort, const std::vector<Node>& terms, std::vector< Node > sterms; std::vector< std::vector< Node > > exp; getSubstitutedTerms( effort, terms, sterms, exp ); + std::map< Node, unsigned > sterm_index; for( unsigned i=0; i<terms.size(); i++ ){ bool processed = false; if( sterms[i]!=terms[i] ){ Node sr = Rewriter::rewrite( sterms[i] ); - if( sr.isConst() ){ + //ask the theory if this term is reduced, e.g. is it constant or it is a non-extf term. + if( d_parent->isExtfReduced( effort, sr, terms[i], exp[i] ) ){ processed = true; markReduced( terms[i] ); Node eq = terms[i].eqNode( sr ); @@ -493,10 +526,25 @@ bool ExtTheory::doInferencesInternal(int effort, const std::vector<Node>& terms, Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq ); Trace("extt-debug") << "...send lemma " << lem << std::endl; if( sendLemma( lem ) ){ - Trace("extt-lemma") << "ExtTheory : Constant rewrite lemma : " << lem << std::endl; + Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem << std::endl; addedLemma = true; } + }else{ + //check if we have already reduced this + std::map< Node, unsigned >::iterator itsi = sterm_index.find( sr ); + if( itsi!=sterm_index.end() ){ + //unsigned j = itsi->second; + //can add (non-reducing) lemma : exp[j] ^ exp[i] => sterms[i] = sterms[j] + //TODO + }else{ + sterm_index[sr] = i; + } + //check if we reduce to another active term? + + Trace("extt-nred") << "Non-reduced term : " << sr << std::endl; } + }else{ + Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl; } if( !processed ){ nred.push_back( terms[i] ); @@ -645,6 +693,13 @@ bool ExtTheory::isContextIndependentInactive(Node n) const { return d_ci_inactive.find(n) != d_ci_inactive.end(); } + +void ExtTheory::getTerms( std::vector< Node >& terms ) { + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + terms.push_back( (*it).first ); + } +} + bool ExtTheory::hasActiveTerm() { return !d_has_extf.get().isNull(); } @@ -685,5 +740,9 @@ std::vector<Node> ExtTheory::getActive(Kind k) const { return active; } +void ExtTheory::clearCache() { + d_gst_cache.clear(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 445d184e4..611e487f1 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -843,6 +843,9 @@ public: return false; } + /* is extended function reduced */ + virtual bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ) { return n.isConst(); } + /** * Get reduction for node * If return value is not 0, then n is reduced. @@ -940,9 +943,6 @@ private: //set of terms from d_ext_func_terms that are SAT-context-independently inactive // (e.g. term t when a reduction lemma of the form t = t' was added) NodeSet d_ci_inactive; - //cache of all lemmas sent - NodeSet d_lemmas; - NodeSet d_pp_lemmas; //watched term for checking if any non-reduced extended functions exist context::CDO< Node > d_has_extf; //extf kind @@ -955,8 +955,21 @@ private: }; std::map< Node, ExtfInfo > d_extf_info; + //cache of all lemmas sent + NodeSet d_lemmas; + NodeSet d_pp_lemmas; + bool d_cacheEnabled; + // if d_cacheEnabled=true : + //cache for getSubstitutedTerms + class SubsTermInfo { + public: + Node d_sterm; + std::vector< Node > d_exp; + }; + std::map< int, std::map< Node, SubsTermInfo > > d_gst_cache; + public: - ExtTheory(Theory* p); + ExtTheory(Theory* p, bool cacheEnabled = false ); virtual ~ExtTheory() {} // add extf kind void addFunctionKind(Kind k) { d_extf_kind[k] = true; } @@ -972,13 +985,13 @@ private: void markReduced( Node n, bool contextDepend = true ); // mark that a and b are congruent terms: set b inactive, set a to inactive if b was inactive void markCongruent( Node a, Node b ); - //getSubstitutedTerms // input : effort, terms // output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i + Node getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache = false ); void getSubstitutedTerms(int effort, const std::vector<Node>& terms, std::vector<Node>& sterms, - std::vector<std::vector<Node> >& exp); + std::vector<std::vector<Node> >& exp, bool useCache = false); // doInferences // * input : effort, terms, batch (whether to send one lemma or lemmas for // all terms) @@ -996,6 +1009,8 @@ private: std::vector<Node>& nred, bool batch = true); bool doReductions(int effort, std::vector<Node>& nred, bool batch = true); + //get the set of terms from d_ext_func_terms + void getTerms( std::vector< Node >& terms ); // has active term bool hasActiveTerm(); // is n active @@ -1004,6 +1019,8 @@ private: std::vector<Node> getActive() const; // get the set of active terms from d_ext_func_terms of kind k std::vector<Node> getActive(Kind k) const; + //clear cache + void clearCache(); }; }/* CVC4::theory namespace */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c7d200a90..ba80b130e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2230,14 +2230,67 @@ void TheoryEngine::checkTheoryAssertionsWithModel() { std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) { TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit; - theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); - theory::Theory* th = theoryOf(tid); + if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){ + //Boolean connective, recurse + std::vector< Node > children; + bool pol = (lit.getKind()!=kind::NOT); + bool is_conjunction = pol==(lit.getKind()==kind::AND); + for( unsigned i=0; i<atom.getNumChildren(); i++ ){ + Node ch = atom[i]; + if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){ + ch = atom[i].negate(); + } + std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects ); + if( chres.first ){ + if( !is_conjunction ){ + return chres; + }else{ + children.push_back( chres.second ); + } + }else if( !chres.first && is_conjunction ){ + return std::pair<bool, Node>(false, Node::null()); + } + } + if( is_conjunction ){ + return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, children)); + }else{ + return std::pair<bool, Node>(false, Node::null()); + } + }else if( atom.getKind()==kind::ITE || ( atom.getKind()==kind::EQUAL && atom[0].getType().isBoolean() ) ){ + bool pol = (lit.getKind()!=kind::NOT); + for( unsigned r=0; r<2; r++ ){ + Node ch = atom[0]; + if( r==1 ){ + ch = ch.negate(); + } + std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects ); + if( chres.first ){ + Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ]; + if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){ + ch2 = ch2.negate(); + } + std::pair<bool, Node> chres2 = entailmentCheck( mode, ch2, params, seffects ); + if( chres2.first ){ + return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second)); + }else{ + break; + } + } + } + return std::pair<bool, Node>(false, Node::null()); + }else{ + //it is a theory atom + theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); + theory::Theory* th = theoryOf(tid); - Assert(th != NULL); - Assert(params == NULL || tid == params->getTheoryId()); - Assert(seffects == NULL || tid == seffects->getTheoryId()); + Assert(th != NULL); + Assert(params == NULL || tid == params->getTheoryId()); + Assert(seffects == NULL || tid == seffects->getTheoryId()); + Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl; - return th->entailmentCheck(lit, params, seffects); + std::pair<bool, Node> chres = th->entailmentCheck(lit, params, seffects); + return chres; + } } void TheoryEngine::spendResource(unsigned ammount) { diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2 index 20a5ca3f0..d5df938a7 100644 --- a/test/regress/regress0/arith/bug716.0.smt2 +++ b/test/regress/regress0/arith/bug716.0.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2 index e457734eb..1c4bbde2b 100644 --- a/test/regress/regress0/arith/div.09.smt2 +++ b/test/regress/regress0/arith/div.09.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect index b21f2d965..4c5aa1491 100644 --- a/test/regress/regress0/expect/scrub.01.smt.expect +++ b/test/regress/regress0/expect/scrub.01.smt.expect @@ -1,6 +1,5 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.02.smt b/test/regress/regress0/expect/scrub.02.smt index f2e6554b7..145801619 100644 --- a/test/regress/regress0/expect/scrub.02.smt +++ b/test/regress/regress0/expect/scrub.02.smt @@ -1,6 +1,5 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect index b21f2d965..4c5aa1491 100644 --- a/test/regress/regress0/expect/scrub.03.smt2.expect +++ b/test/regress/regress0/expect/scrub.03.smt2.expect @@ -1,6 +1,5 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.04.smt2 b/test/regress/regress0/expect/scrub.04.smt2 index e457734eb..1c4bbde2b 100644 --- a/test/regress/regress0/expect/scrub.04.smt2 +++ b/test/regress/regress0/expect/scrub.04.smt2 @@ -1,6 +1,5 @@ ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n) -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc index b9cb1cd8a..896149334 100644 --- a/test/regress/regress0/expect/scrub.06.cvc +++ b/test/regress/regress0/expect/scrub.06.cvc @@ -1,9 +1,8 @@ % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^$/d' -% EXPECT: A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% EXPECT: A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXIT: 1 n : REAL; -QUERY (n/n) = 1;
\ No newline at end of file +QUERY (n/n) = 1; diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect index dfcd45a8a..4c5aa1491 100644 --- a/test/regress/regress0/expect/scrub.07.sy.expect +++ b/test/regress/regress0/expect/scrub.07.sy.expect @@ -1,6 +1,5 @@ -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 3b9574cdf..7f78dbc48 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,7 +1,6 @@ ; COMMAND-LINE: --cegqi-si=all --no-dump-synth -; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM ; EXPECT: ") ; EXIT: 1 @@ -10,4 +9,4 @@ (synth-fun f ((n Int)) Int) (constraint (= (/ n n) 1)) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p index 17eef44fe..ee765a91a 100644 --- a/test/regress/regress0/expect/scrub.09.p +++ b/test/regress/regress0/expect/scrub.09.p @@ -1,7 +1,6 @@ % COMMAND-LINE: --cegqi-si=all --no-dump-synth -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM -% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option. +% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM % EXPECT: ") % EXIT: 1 |