This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.
This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.
This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.
The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).
<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
<< endl;
dumpAssertions("pre-definition-expansion", assertions);
- d_exDefs.expandAssertions(assertions, false);
+ // Expand definitions, which replaces defined functions with their definition
+ // and does beta reduction. Notice we pass true as the second argument since
+ // we do not want to call theories to expand definitions here, since we want
+ // to give the opportunity to rewrite/preprocess terms before expansion.
+ d_exDefs.expandAssertions(assertions, true);
Trace("smt-proc")
<< "ProcessAssertions::processAssertions() : post-definition-expansion"
<< endl;
: d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
{
}
-TrustNode ArithPreprocess::eliminate(TNode n) { return d_opElim.eliminate(n); }
+TrustNode ArithPreprocess::eliminate(TNode n, bool partialOnly)
+{
+ return d_opElim.eliminate(n, partialOnly);
+}
bool ArithPreprocess::reduceAssertion(TNode atom)
{
context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
* Call eliminate operators on formula n, return the resulting trust node,
* which is of TrustNodeKind REWRITE and whose node is the result of
* eliminating extended operators from n.
+ *
+ * @param n The node to eliminate operators from
+ * @param partialOnly Whether we are eliminating partial operators only.
+ * @return the trust node proving (= n nr) where nr is the return of
+ * eliminating operators in n, or the null trust node if n was unchanged.
*/
- TrustNode eliminate(TNode n);
+ TrustNode eliminate(TNode n, bool partialOnly = false);
/**
* Reduce assertion. This sends a lemma via the inference manager if atom
* contains any extended operators. When applicable, the lemma is of the form:
}
}
-TrustNode OperatorElim::eliminate(Node n)
+TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
{
TConvProofGenerator* tg = nullptr;
- Node nn = eliminateOperators(n, tg);
+ Node nn = eliminateOperators(n, tg, partialOnly);
if (nn != n)
{
// since elimination may introduce new operators to eliminate, we must
// recursively eliminate result
- Node nnr = eliminateOperatorsRec(nn, tg);
+ Node nnr = eliminateOperatorsRec(nn, tg, partialOnly);
return TrustNode::mkTrustRewrite(n, nnr, nullptr);
}
return TrustNode::null();
}
-Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperatorsRec(Node n,
+ TConvProofGenerator* tg,
+ bool partialOnly)
{
Trace("arith-elim") << "Begin elim: " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
{
ret = nm->mkNode(cur.getKind(), children);
}
- Node retElim = eliminateOperators(ret, tg);
+ Node retElim = eliminateOperators(ret, tg, partialOnly);
if (retElim != ret)
{
// recursively eliminate operators in result, since some eliminations
// are defined in terms of other non-standard operators.
- ret = eliminateOperatorsRec(retElim, tg);
+ ret = eliminateOperatorsRec(retElim, tg, partialOnly);
}
visited[cur] = ret;
}
return visited[n];
}
-Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperators(Node node,
+ TConvProofGenerator* tg,
+ bool partialOnly)
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
case TO_INTEGER:
case IS_INTEGER:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
Node toIntSkolem;
std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]);
if (it == d_to_int_skolem.end())
case INTS_DIVISION_TOTAL:
case INTS_MODULUS_TOTAL:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
Node den = Rewriter::rewrite(node[1]);
Node num = Rewriter::rewrite(node[0]);
Node intVar;
}
case DIVISION_TOTAL:
{
+ if (partialOnly)
+ {
+ // not eliminating total operators
+ return node;
+ }
Node num = Rewriter::rewrite(node[0]);
Node den = Rewriter::rewrite(node[1]);
if (den.isConst())
* transcendental functions), then we replace it by a form that eliminates
* that operator. This may involve the introduction of witness terms.
*/
- TrustNode eliminate(Node n);
+ TrustNode eliminate(Node n, bool partialOnly = false);
/**
* Get axiom for term n. This returns the axiom that this class uses to
* eliminate the term n, which is determined by its top-most symbol.
* @param n The node to eliminate operators from.
* @return The (single step) eliminated form of n.
*/
- Node eliminateOperators(Node n, TConvProofGenerator* tg);
+ Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
/**
* Recursively ensure that n has no non-standard operators. This applies
* the above method on all subterms of n.
* @param n The node to eliminate operators from.
* @return The eliminated form of n.
*/
- Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg);
+ Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg, bool partialOnly);
/** get arithmetic skolem
*
* Returns the Skolem in the above map for the given id, creating it if it
d_internal->preRegisterTerm(n);
}
+TrustNode TheoryArith::expandDefinition(Node node)
+{
+ // call eliminate operators, to eliminate partial operators only
+ return d_arithPreproc.eliminate(node, true);
+}
+
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
TrustNode TheoryArith::ppRewrite(TNode atom)
// theories may generate lemmas that involve non-standard operators. For
// example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
// introduce non-standard arithmetic terms appearing in grammars.
- // call eliminate operators
- return d_arithPreproc.eliminate(n);
+ // call eliminate operators. In contrast to expandDefinitions, we eliminate
+ // *all* extended arithmetic operators here, including total ones.
+ return d_arithPreproc.eliminate(n, false);
}
Theory::PPAssertStatus TheoryArith::ppAssert(
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
-
+ /**
+ * Expand definition, which eliminates extended operators like div/mod in
+ * the given node.
+ */
+ TrustNode expandDefinition(Node node) override;
/**
* Does non-context dependent setup for a node connected to a theory.
*/
TrustNode TheoryArrays::ppRewrite(TNode term)
{
+ // first, see if we need to expand definitions
+ TrustNode texp = expandDefinition(term);
+ if (!texp.isNull())
+ {
+ return texp;
+ }
if (!d_preprocess)
{
return TrustNode::null();
return d_internal->ppAssert(tin, outSubstitutions);
}
-TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
+TrustNode TheoryBV::ppRewrite(TNode t)
+{
+ // first, see if we need to expand definitions
+ TrustNode texp = expandDefinition(t);
+ if (!texp.isNull())
+ {
+ return texp;
+ }
+ return d_internal->ppRewrite(t);
+}
void TheoryBV::presolve() { d_internal->presolve(); }
{
Trace("datatypes-prereg")
<< "TheoryDatatypes::preRegisterTerm() " << n << endl;
+ // external selectors should be preprocessed away by now
+ Assert(n.getKind() != APPLY_SELECTOR);
// must ensure the type is well founded and has no nested recursion if
// the option dtNestedRec is not set to true.
TypeNode tn = n.getType();
TrustNode TheoryDatatypes::ppRewrite(TNode in)
{
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
-
+ // first, see if we need to expand definitions
+ TrustNode texp = expandDefinition(in);
+ if (!texp.isNull())
+ {
+ return texp;
+ }
if( in.getKind()==EQUAL ){
Node nn;
std::vector< Node > rew;
TrustNode TheoryFp::ppRewrite(TNode node)
{
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
+ // first, see if we need to expand definitions
+ TrustNode texp = expandDefinition(node);
+ if (!texp.isNull())
+ {
+ return texp;
+ }
Node res = node;
// already processed variable
continue;
}
- if (ces.getType().isBoolean())
+ // must avoid selector symbols, and function skolems introduced by
+ // theory preprocessing
+ TypeNode ct = ces.getType();
+ if (ct.isBoolean() || ct.isFunctionLike())
{
// Boolean variables, including the counterexample literal, don't matter
// since they are always assigned a model value.
{
return;
}
+ Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
NodeManager* nm = NodeManager::currentNM();
FirstOrderModel* m = d_quantEngine->getModel();
std::vector<Node> lemmas;
++it)
{
Node q = it->first;
+ Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
&& d_added_split.find(q) == d_added_split.end())
{
Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
d_quantEngine->addLemma(lem, false);
}
+ Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
}
d_valuation.setUnevaluatedKind(COMPREHENSION);
// choice is used to eliminate witness
d_valuation.setUnevaluatedKind(WITNESS);
+ // Universe set is not evaluated. This is moreover important for ensuring that
+ // we do not eliminate terms whose value involves the universe set.
+ d_valuation.setUnevaluatedKind(UNIVERSE_SET);
// functions we are doing congruence over
d_equalityEngine->addFunctionKind(SINGLETON);
}
TrustNode TheorySets::expandDefinition(Node n)
+{
+ return d_internal->expandDefinition(n);
+}
+
+TrustNode TheorySets::ppRewrite(TNode n)
{
Kind nk = n.getKind();
if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
throw LogicException(ss.str());
}
}
- return d_internal->expandDefinition(n);
+ // just expand definitions
+ return expandDefinition(n);
}
Theory::PPAssertStatus TheorySets::ppAssert(
std::string identify() const override { return "THEORY_SETS"; }
void preRegisterTerm(TNode node) override;
TrustNode expandDefinition(Node n) override;
+ TrustNode ppRewrite(TNode n) override;
PPAssertStatus ppAssert(TrustNode tin,
TrustSubstitutionMap& outSubstitutions) override;
void presolve() override;
TrustNode TheoryStrings::ppRewrite(TNode atom)
{
Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+ // first, see if we need to expand definitions
+ TrustNode texp = expandDefinition(atom);
+ if (!texp.isNull())
+ {
+ return texp;
+ }
TrustNode ret;
Node atomRet = atom;
if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
// get the node
Node node = tlemma.getNode();
Node lemma = tlemma.getProven();
- Trace("te-lemma") << "Lemma, input: " << lemma << std::endl;
+ Trace("te-lemma") << "Lemma, input: " << lemma << ", property = " << p
+ << std::endl;
Assert(!expr::hasFreeVar(lemma));
regress1/quantifiers/smtlib46f14a.smt2
regress1/quantifiers/smtlibe99bbe.smt2
regress1/quantifiers/smtlibf957ea.smt2
- regress1/quantifiers/stream-x2014-09-18-unsat.smt2
regress1/quantifiers/sygus-infer-nested.smt2
regress1/quantifiers/symmetric_unsat_7.smt2
regress1/quantifiers/var-eq-trigger.smt2
regress2/bv_to_int_5095_2.smt2
regress2/bv_to_int_ashr.smt2
regress2/bv_to_int_bitwise.smt2
- regress2/bv_to_int_bvmul1.smt2
regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
regress2/bv_to_int_inc1.smt2
regress2/bv_to_int_mask_array_1.smt2
regress1/quantifiers/nl-pow-trick.smt2
# timeout after changes to nonlinear on PR #5351
regress1/quantifiers/rel-trigger-unusable.smt2
+ # changes to expand definitions, related to trigger selection for selectors
+ regress1/quantifiers/stream-x2014-09-18-unsat.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/subtype-param-unk.smt2
regress1/quantifiers/subtype-param.smt2
# timeout on debug
regress2/arith/real2int-test.smt2
regress2/bug396.smt2
+ # due to bv2int not handling unsigned/signed division
+ regress2/bv_to_int_bvmul1.smt2
regress2/nl/dumortier-050317.smt2
regress2/nl/nt-lemmas-bad.smt2
regress2/quantifiers/ForElimination-scala-9.smt2
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic QF_LIA)
(set-info :status sat)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic QF_NIA)
(declare-fun a () Int)
(declare-fun e () Int)
+; COMMAND-LINE: -q
; EXPECT: sat
; Preamble --------------
+% COMMAND-LINE: -q
% EXPECT: sat
Ints_0 : ARRAY INT OF INT;
C : TYPE = [# i : INT #];
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
; EXPECT: sat
; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
(set-logic ALL_SUPPORTED)
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic QF_AUFNRA)
(set-info :status sat)
(declare-const arr0 (Array Real Real))
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic QF_AUFNRA)
(set-info :status sat)
(declare-const a (Array Real Real))
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
-; COMMAND-LINE: --fmf-bound --no-cegqi
+; COMMAND-LINE: --fmf-bound --no-cegqi -q
; EXPECT: sat
(set-logic ALL)
(assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0))))
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))
+% COMMAND-LINE: -q
% EXPECT: sat
OPTION "produce-models";
OPTION "fmf-bound";
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(declare-sort b__ 0)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic AUFBV)
(set-info :status sat)
(set-option :bv-div-zero-const false)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic NIA)
(set-option :strings-exp true)
(set-info :status sat)
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-fun S () (Set Int))
(assert (= (singleton x) S))
(assert (is_singleton S))
(assert (is_singleton (singleton 3)))
-(check-sat)
\ No newline at end of file
+(check-sat)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(declare-fun s () (Set Int))
+% COMMAND-LINE: -q
% EXPECT: sat
OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";
+; COMMAND-LINE: --produce-models
; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
; EXIT: 1
(set-logic ALL)
; EXPECT: sat
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference -q
(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Int)
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find -q
% EXPECT: sat
DATATYPE
myType = A | B
; EXPECT: sat
-; COMMAND --solve-bv-as-int=sum
+; COMMAND-LINE: --solve-bv-as-int=sum -q
(set-logic BV)
(declare-const bv_42-0 (_ BitVec 42))
(assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28)))
-(check-sat)
\ No newline at end of file
+(check-sat)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic UFDTLIRA)
(set-option :fmf-bound true)
(set-option :finite-model-find true)
projects / cvc5.git / commitdiff