#include "theory/arith/nl_model.h"
#include "expr/node_algorithm.h"
+#include "options/arith_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/rewriter.h"
NlModel::~NlModel() {}
-void NlModel::reset(TheoryModel* m)
+void NlModel::reset(TheoryModel* m, std::map<Node, Node>& arithModel)
{
d_model = m;
d_mv[0].clear();
d_mv[1].clear();
+ d_arithVal.clear();
+ // process arithModel
+ std::map<Node, Node>::iterator it;
+ for (const std::pair<const Node, Node>& m : arithModel)
+ {
+ d_arithVal[m.first] = m.second;
+ }
}
void NlModel::resetCheck()
return ret;
}
-Node NlModel::getValueInternal(Node n) const
-{
- return d_model->getValue(n);
-}
-
bool NlModel::hasTerm(Node n) const
{
- return d_model->hasTerm(n);
+ return d_arithVal.find(n) != d_arithVal.end();
}
Node NlModel::getRepresentative(Node n) const
{
+ if (n.isConst())
+ {
+ return n;
+ }
+ std::map<Node, Node>::const_iterator it = d_arithVal.find(n);
+ if (it != d_arithVal.end())
+ {
+ AlwaysAssert(it->second.isConst());
+ return it->second;
+ }
return d_model->getRepresentative(n);
}
+Node NlModel::getValueInternal(Node n) const
+{
+ if (n.isConst())
+ {
+ return n;
+ }
+ std::map<Node, Node>::const_iterator it = d_arithVal.find(n);
+ if (it != d_arithVal.end())
+ {
+ AlwaysAssert(it->second.isConst());
+ return it->second;
+ }
+ // It is unconstrained in the model, return 0.
+ return d_zero;
+}
+
int NlModel::compare(Node i, Node j, bool isConcrete, bool isAbsolute)
{
Node ci = computeModelValue(i, isConcrete);
* where m is the model of the theory of arithmetic. This method resets the
* cache of computed model values.
*/
- void reset(TheoryModel* m);
+ void reset(TheoryModel* m, std::map<Node, Node>& arithModel);
/** reset check
*
* This method is called when the non-linear arithmetic solver restarts
Node d_true;
Node d_false;
Node d_null;
+ /**
+ * The values that the arithmetic theory solver assigned in the model. This
+ * corresponds to exactly the set of equalities that TheoryArith is currently
+ * sending to TheoryModel during collectModelInfo.
+ */
+ std::map<Node, Node> d_arithVal;
/** cache of model values
*
* Stores the the concrete/abstract model values. This is a cache of the
eq::EqualityEngine* ee)
: d_lemmas(containing.getUserContext()),
d_zero_split(containing.getUserContext()),
- d_skolem_atoms(containing.getUserContext()),
d_containing(containing),
d_ee(ee),
d_needsLastCall(false),
for (size_t i = 0; i < assertions.size(); ++i) {
Node lit = assertions[i];
Node atom = lit.getKind()==NOT ? lit[0] : lit;
- if( d_skolem_atoms.find( atom )==d_skolem_atoms.end() ){
- Node litv = d_model.computeConcreteModelValue(lit);
- Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv;
- if (litv != d_true) {
- Trace("nl-ext-mv-assert") << " [model-false]" << std::endl;
- //Assert(litv == d_false);
- false_asserts.push_back(lit);
- } else {
- Trace("nl-ext-mv-assert") << std::endl;
- }
+ Node litv = d_model.computeConcreteModelValue(lit);
+ Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv;
+ if (litv != d_true)
+ {
+ Trace("nl-ext-mv-assert") << " [model-false]" << std::endl;
+ false_asserts.push_back(lit);
+ }
+ else
+ {
+ Trace("nl-ext-mv-assert") << std::endl;
}
}
return false_asserts;
}
else
{
- std::map<Node, Node> approximations;
- std::map<Node, Node> arithModel;
- TheoryModel* tm = d_containing.getValuation().getModel();
- if (!d_builtModel.get())
+ // If we computed lemmas during collectModelInfo, send them now.
+ if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty())
{
- // run a last call effort check
- std::vector<Node> mlems;
- std::vector<Node> mlemsPp;
- if (modelBasedRefinement(mlems, mlemsPp))
- {
- sendLemmas(mlems);
- sendLemmas(mlemsPp, true);
- return;
- }
+ sendLemmas(d_cmiLemmas);
+ sendLemmas(d_cmiLemmasPp, true);
+ return;
}
- // get the values that should be replaced in the model
- d_model.getModelValueRepair(arithModel, approximations);
- // those that are exact are written as exact approximations to the model
- for (std::pair<const Node, Node>& r : arithModel)
- {
- Node eq = r.first.eqNode(r.second);
- eq = Rewriter::rewrite(eq);
- tm->recordApproximation(r.first, eq);
- }
- // those that are approximate are recorded as approximations
- for (std::pair<const Node, Node>& a : approximations)
+ // Otherwise, we will answer SAT. The values that we approximated are
+ // recorded as approximations here.
+ TheoryModel* tm = d_containing.getValuation().getModel();
+ for (std::pair<const Node, Node>& a : d_approximations)
{
tm->recordApproximation(a.first, a.second);
}
bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems,
std::vector<Node>& mlemsPp)
{
- // reset the model object
- d_model.reset(d_containing.getValuation().getModel());
// get the assertions
std::vector<Node> assertions;
getAssertions(assertions);
return false;
}
+void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
+{
+ if (!needsCheckLastEffort())
+ {
+ // no non-linear constraints, we are done
+ return;
+ }
+ d_model.reset(d_containing.getValuation().getModel(), arithModel);
+ // run a last call effort check
+ d_cmiLemmas.clear();
+ d_cmiLemmasPp.clear();
+ if (!d_builtModel.get())
+ {
+ modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp);
+ }
+ if (d_builtModel.get())
+ {
+ d_approximations.clear();
+ // modify the model values
+ d_model.getModelValueRepair(arithModel, d_approximations);
+ }
+}
+
void NonlinearExtension::presolve()
{
Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
Node atom = lit.getKind() == NOT ? lit[0] : lit;
Node litv = d_model.computeConcreteModelValue(lit);
bool considerLit = false;
- if( d_skolem_atoms.find(atom) != d_skolem_atoms.end() )
- {
- //always consider skolem literals
- considerLit = true;
- }
- else
- {
- // Only consider literals that are in false_asserts.
- considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit)
- != false_asserts.end();
- }
+ // Only consider literals that are in false_asserts.
+ considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit)
+ != false_asserts.end();
if (considerLit)
{
Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl;
Node conc_lit = NodeManager::currentNM()->mkNode( atom.getKind(), polyn, d_zero );
conc_lit = Rewriter::rewrite( conc_lit );
- d_skolem_atoms.insert( conc_lit );
if( !polarity ){
conc_lit = conc_lit.negate();
}
if( itf==d_factor_skolem.end() ){
Node k = NodeManager::currentNM()->mkSkolem( "kf", n.getType() );
Node k_eq = Rewriter::rewrite( k.eqNode( n ) );
- d_skolem_atoms.insert( k_eq );
lemmas.push_back( k_eq );
d_factor_skolem[n] = k;
return k;
*
* This call may result in (possibly multiple) calls to d_out->lemma(...)
* where d_out is the output channel of TheoryArith.
+ *
+ * If e is FULL, then we add lemmas based on context-depedent
+ * simplification (see Reynolds et al FroCoS 2017).
+ *
+ * If e is LAST_CALL, we add lemmas based on model-based refinement
+ * (see additionally Cimatti et al., TACAS 2017). The lemmas added at this
+ * effort may be computed during a call to interceptModel as described below.
*/
void check(Theory::Effort e);
+ /** intercept model
+ *
+ * This method is called during TheoryArith::collectModelInfo, which is
+ * invoked after the linear arithmetic solver passes a full effort check
+ * with no lemmas.
+ *
+ * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn }
+ * which represents the linear arithmetic theory solver's contribution to the
+ * current candidate model. That is, its collectModelInfo method is requesting
+ * that equalities v1 = c1, ..., vn = cn be added to the current model, where
+ * v1, ..., vn are arithmetic variables and c1, ..., cn are constants. Notice
+ * arithmetic variables may be real-valued terms belonging to other theories,
+ * or abstractions of applications of multiplication (kind NONLINEAR_MULT).
+ *
+ * This method requests that the non-linear solver inspect this model and
+ * do any number of the following:
+ * (1) Construct lemmas based on a model-based refinement procedure inspired
+ * by Cimatti et al., TACAS 2017.,
+ * (2) In the case that the nonlinear solver finds that the current
+ * constraints are satisfiable, it may "repair" the values in the argument
+ * arithModel so that it satisfies certain nonlinear constraints. This may
+ * involve e.g. solving for variables in nonlinear equations.
+ *
+ * Notice that in the former case, the lemmas it constructs are not sent out
+ * immediately. Instead, they are put in temporary vectors d_cmiLemmas
+ * and d_cmiLemmasPp, which are then sent out (if necessary) when a last call
+ * effort check is issued to this class.
+ */
+ void interceptModel(std::map<Node, Node>& arithModel);
/** Does this class need a call to check(...) at last call effort? */
bool needsCheckLastEffort() const { return d_needsLastCall; }
/** presolve
NodeSet d_lemmas;
/** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */
NodeSet d_zero_split;
-
- /**
- * The set of atoms with Skolems that this solver introduced. We do not
- * require that models satisfy literals over Skolem atoms.
- */
- NodeSet d_skolem_atoms;
/** commonly used terms */
Node d_zero;
* and for establishing when we are able to answer "SAT".
*/
NlModel d_model;
+ /**
+ * The lemmas we computed during collectModelInfo. We store two vectors of
+ * lemmas to be sent out on the output channel of TheoryArith. The first
+ * is not preprocessed, the second is.
+ */
+ std::vector<Node> d_cmiLemmas;
+ std::vector<Node> d_cmiLemmasPp;
+ /** The approximations computed during collectModelInfo. */
+ std::map<Node, Node> d_approximations;
/** have we successfully built the model in this SAT context? */
context::CDO<bool> d_builtModel;
if(effortLevel == Theory::EFFORT_LAST_CALL){
if( options::nlExt() ){
- d_nonlinearExtension->check( effortLevel );
+ d_nonlinearExtension->check(effortLevel);
}
return;
}
// TODO:
// This is not very good for user push/pop....
// Revisit when implementing push/pop
+ // Map of terms to values, constructed when non-linear arithmetic is active.
+ std::map<Node, Node> arithModel;
for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
ArithVar v = *vi;
Node qNode = mkRationalNode(qmodel);
Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
-
- if (!m->assertEquality(term, qNode, true))
+ if (options::nlExt())
{
- return false;
+ // Let non-linear extension inspect the values before they are sent
+ // to the theory model.
+ arithModel[term] = qNode;
+ }
+ else
+ {
+ if (!m->assertEquality(term, qNode, true))
+ {
+ return false;
+ }
}
}else{
Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
}
}
}
+ if (options::nlExt())
+ {
+ // Non-linear may repair values to satisfy non-linear constraints (see
+ // documentation for NonlinearExtension::interceptModel).
+ d_nonlinearExtension->interceptModel(arithModel);
+ // We are now ready to assert the model.
+ for (std::pair<const Node, Node>& p : arithModel)
+ {
+ if (!m->assertEquality(p.first, p.second, true))
+ {
+ return false;
+ }
+ }
+ }
// Iterate over equivalence classes in LinearEqualityModule
// const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
regress0/model-core.smt2
regress0/nl/coeff-sat.smt2
regress0/nl/ext-rew-aggr-test.smt2
+ regress0/nl/issue3003.smt2
regress0/nl/issue3407.smt2
+ regress0/nl/issue3411.smt2
regress0/nl/issue3475.smt2
regress0/nl/magnitude-wrong-1020-m.smt2
regress0/nl/mult-po.smt2
regress0/nl/nta/tan-rewrite.smt2
regress0/nl/real-as-int.smt2
regress0/nl/real-div-ufnra.smt2
+ regress0/nl/sin-cos-346-b-chunk-0169.smt2
regress0/nl/sqrt.smt2
regress0/nl/sqrt2-value.smt2
regress0/nl/subs0-unsat-confirm.smt2
regress1/nl/exp1-lb.smt2
regress1/nl/exp_monotone.smt2
regress1/nl/factor_agg_s.smt2
+ regress1/nl/issue3441.smt2
regress1/nl/metitarski-1025.smt2
regress1/nl/metitarski-3-4.smt2
regress1/nl/metitarski_3_4_2e.smt2
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun _substvar_15_ () Real)
+(declare-fun _substvar_17_ () Real)
+(assert (let ((?v_1 (<= 0.0 _substvar_15_))) (and ?v_1 (and ?v_1 (and ?v_1 (= (* _substvar_15_ _substvar_15_) (+ 1 (* _substvar_17_ (* _substvar_17_ (- 1))))))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= (/ 0 (+ 1 (* a a b))) 0))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoX () Real)
+(declare-fun skoSQ3 () Real)
+(declare-fun pi () Real)
+(assert (let ((?v_0 (* skoSQ3 skoSQ3))) (and (not (<= (* skoX (* skoX (* skoX (* skoX (+ (/ 1 24) (* skoX (* skoX (+ (/ (- 1) 720) (* skoX (* skoX (/ 1 40320))))))))))) (+ (- 3) ?v_0))) (and (= ?v_0 3) (and (not (<= (+ (/ (- 1) 10000000) (* pi (/ 1 2))) skoX)) (and (not (<= pi (/ 15707963 5000000))) (and (not (<= (/ 31415927 10000000) pi)) (and (not (<= skoX 0)) (not (<= skoSQ3 0))))))))))
+(check-sat)
+(exit)
--- /dev/null
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+(assert (and (>= (+ (* b c (- (- 4) d)) (- 1)) 0 (div a b))))
+(check-sat)
projects / cvc5.git / commitdiff