category = "regular"
long = "quant-dsplit-mode=MODE"
type = "CVC4::theory::quantifiers::QuantDSplitMode"
- default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
+ default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT"
handler = "stringToQuantDSplitMode"
includes = ["options/quantifiers_modes.h"]
help = "mode for dynamic quantifiers splitting"
{
int max_index = -1;
int max_score = -1;
- if( q.getNumChildren()==3 ){
- return;
- }
Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
TypeNode tn = q[0][i].getType();
if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0;
}else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
- //only split if goes from being unhandled -> handled by finite instantiation
- // an example is datatypes with uninterpreted sort fields, which are "interpreted finite" but not "finite"
if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
- score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1;
+ if (dt.isInterpretedFinite(tn.toType()))
+ {
+ // split if goes from being unhandled -> handled by finite
+ // instantiation. An example is datatypes with uninterpreted sort
+ // fields which are "interpreted finite" but not "finite".
+ score = 1;
+ }
+ else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
+ {
+ // split if only one constructor
+ score = 1;
+ }
}
}
Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl;
void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
{
//add lemmas ASAP (they are a reduction)
- if (quant_e == QEFFORT_CONFLICT)
+ if (quant_e != QEFFORT_CONFLICT)
{
- std::vector< Node > lemmas;
- for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
- Node q = it->first;
- if( d_quantEngine->getModel()->isQuantifierAsserted( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
- if( d_added_split.find( q )==d_added_split.end() ){
- d_added_split.insert( q );
- std::vector< Node > bvs;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- if( (int)i!=it->second ){
- bvs.push_back( q[0][i] );
- }
- }
- std::vector< Node > disj;
- disj.push_back( q.negate() );
- TNode svar = q[0][it->second];
- TypeNode tn = svar.getType();
- if( tn.isDatatype() ){
- std::vector< Node > cons;
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
- std::vector< Node > vars;
- for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
- TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
- Node v = NodeManager::currentNM()->mkBoundVar( tns );
- vars.push_back( v );
- }
- std::vector< Node > bvs_cmb;
- bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
- bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
- vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
- Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
- TNode ct = c;
- Node body = q[1].substitute( svar, ct );
- if( !bvs_cmb.empty() ){
- body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
- }
- cons.push_back( body );
- }
- Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons );
- disj.push_back( conc );
- }else{
- Assert( false );
+ return;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ FirstOrderModel* m = d_quantEngine->getModel();
+ std::vector<Node> lemmas;
+ for (std::map<Node, int>::iterator it = d_quant_to_reduce.begin();
+ it != d_quant_to_reduce.end();
+ ++it)
+ {
+ Node q = it->first;
+ if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
+ && d_added_split.find(q) == d_added_split.end())
+ {
+ d_added_split.insert(q);
+ std::vector<Node> bvs;
+ for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+ {
+ if (static_cast<int>(i) != it->second)
+ {
+ bvs.push_back(q[0][i]);
+ }
+ }
+ std::vector<Node> disj;
+ disj.push_back(q.negate());
+ TNode svar = q[0][it->second];
+ TypeNode tn = svar.getType();
+ Assert(tn.isDatatype());
+ std::vector<Node> cons;
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+ {
+ std::vector<Node> vars;
+ for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
+ {
+ TypeNode tns = TypeNode::fromType(dt[j][k].getRangeType());
+ Node v = nm->mkBoundVar(tns);
+ vars.push_back(v);
+ }
+ std::vector<Node> bvs_cmb;
+ bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
+ bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
+ vars.insert(vars.begin(), Node::fromExpr(dt[j].getConstructor()));
+ Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
+ TNode ct = c;
+ Node body = q[1].substitute(svar, ct);
+ if (!bvs_cmb.empty())
+ {
+ Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs_cmb);
+ std::vector<Node> children;
+ children.push_back(bvl);
+ children.push_back(body);
+ if (q.getNumChildren() == 3)
+ {
+ Node ipls = q[2].substitute(svar, ct);
+ children.push_back(ipls);
}
- lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
+ body = nm->mkNode(kind::FORALL, children);
}
+ cons.push_back(body);
}
+ Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(kind::AND, cons);
+ disj.push_back(conc);
+ lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(kind::OR, disj));
}
+ }
- //add lemmas to quantifiers engine
- for( unsigned i=0; i<lemmas.size(); i++ ){
- Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
- d_quantEngine->addLemma( lemmas[i], false );
- }
- //d_quant_to_reduce.clear();
+ // add lemmas to quantifiers engine
+ for (const Node& lem : lemmas)
+ {
+ Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
+ d_quantEngine->addLemma(lem, false);
}
}
namespace quantifiers {
+/** Quantifiers dynamic splitting
+ *
+ * This module identifies quantified formulas that should be "split", e.g.
+ * based on datatype constructor case splitting.
+ *
+ * An example of a quantified formula that we may split is the following. Let:
+ * optionPair := mkPair( U, U ) | none
+ * where U is an uninterpreted sort. The quantified formula:
+ * forall x : optionPair. P( x )
+ * may be "split" via the lemma:
+ * forall x : optionPair. P( x ) <=>
+ * ( forall xy : U. P( mkPair( x, y ) ) OR P( none ) )
+ *
+ * Notice that such splitting may lead to exponential behavior, say if we
+ * quantify over 32 variables of type optionPair above gives 2^32 disjuncts.
+ * This class is used to compute this splitting dynamically, by splitting
+ * one variable per quantified formula at a time.
+ */
class QuantDSplit : public QuantifiersModule {
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
- /** list of relevant quantifiers asserted in the current context */
- std::map< Node, int > d_quant_to_reduce;
- /** whether we have instantiated quantified formulas */
- NodeSet d_added_split;
-public:
+
+ public:
QuantDSplit( QuantifiersEngine * qe, context::Context* c );
/** determine whether this quantified formula will be reduced */
void checkOwnership(Node q) override;
-
/* whether this module needs to check this round */
bool needsCheck(Theory::Effort e) override;
/* Call during quantifier engine's check */
void check(Theory::Effort e, QEffort quant_e) override;
- /* Called for new quantifiers */
- void registerQuantifier(Node q) override {}
- void assertNode(Node n) override {}
+ /** check complete for */
bool checkCompleteFor(Node q) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const override { return "QuantDSplit"; }
+
+ private:
+ /** list of relevant quantifiers asserted in the current context */
+ std::map<Node, int> d_quant_to_reduce;
+ /** whether we have instantiated quantified formulas */
+ NodeSet d_added_split;
};
}
}
}
}
+ else if (lit.getKind() == APPLY_TESTER && pol
+ && lit[0].getKind() == BOUND_VARIABLE && options::dtVarExpandQuant())
+ {
+ Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
+ << std::endl;
+ Expr testerExpr = lit.getOperator().toExpr();
+ unsigned index = Datatype::indexOf(testerExpr);
+ Node s = datatypeExpand(index, lit[0], args);
+ if (!s.isNull())
+ {
+ vars.push_back(lit[0]);
+ subs.push_back(s);
+ Trace("var-elim-dt") << "...apply substitution " << s << "/" << lit[0]
+ << std::endl;
+ return true;
+ }
+ }
if (lit.getKind() == BOUND_VARIABLE)
{
std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
return false;
}
+Node QuantifiersRewriter::datatypeExpand(unsigned index,
+ Node v,
+ std::vector<Node>& args)
+{
+ if (!v.getType().isDatatype())
+ {
+ return Node::null();
+ }
+ std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
+ if (ita == args.end())
+ {
+ return Node::null();
+ }
+ const Datatype& dt =
+ static_cast<DatatypeType>(v.getType().toType()).getDatatype();
+ Assert(index < dt.getNumConstructors());
+ const DatatypeConstructor& c = dt[index];
+ std::vector<Node> newChildren;
+ newChildren.push_back(Node::fromExpr(c.getConstructor()));
+ std::vector<Node> newVars;
+ for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+ {
+ TypeNode tn = TypeNode::fromType(c.getArgType(j));
+ Node vn = NodeManager::currentNM()->mkBoundVar(tn);
+ newChildren.push_back(vn);
+ newVars.push_back(vn);
+ }
+ args.erase(ita);
+ args.insert(args.end(), newVars.begin(), newVars.end());
+ return NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, newChildren);
+}
+
bool QuantifiersRewriter::getVarElim(Node n,
bool pol,
std::vector<Node>& args,
std::map< Node, Node >& cache, std::map< Node, Node >& icache,
std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
+ /** datatype expand
+ *
+ * If v occurs in args and has a datatype type whose index^th constructor is
+ * C, this method returns a node of the form C( x1, ..., xn ), removes v from
+ * args and adds x1...xn to args.
+ */
+ static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args);
//-------------------------------------variable elimination
/** is variable elimination
*
regress1/quantifiers/dump-inst.smt2
regress1/quantifiers/ext-ex-deq-trigger.smt2
regress1/quantifiers/extract-nproc.smt2
+ regress1/quantifiers/f993-loss-easy.smt2
regress1/quantifiers/florian-case-ax.smt2
regress1/quantifiers/fp-cegqi-unsat.smt2
regress1/quantifiers/gauss_init_0030.fof.smt2
regress1/quantifiers/is-even.smt2
regress1/quantifiers/isaplanner-goal20.smt2
regress1/quantifiers/issue2970-string-var-elim.smt2
+ regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lra-vts-inf.smt2
regress1/quantifiers/mix-coeff.smt2
--- /dev/null
+(set-info :smt-lib-version 2.6)
+(set-logic UFDT)
+(set-info :status unsat)
+(declare-sort A$ 0)
+(declare-sort Nat$ 0)
+(declare-sort Nat_nat_fun$ 0)
+(declare-sort Enat_nat_fun$ 0)
+(declare-sort Nat_bool_fun$ 0)
+(declare-sort Nat_enat_fun$ 0)
+(declare-sort Bool_bool_fun$ 0)
+(declare-sort Enat_bool_fun$ 0)
+(declare-sort Enat_enat_fun$ 0)
+(declare-sort A_stream_bool_fun$ 0)
+(declare-sort Nat_bool_fun_nat_fun$ 0)
+(declare-sort Nat_nat_bool_fun_fun$ 0)
+(declare-sort Bool_enat_bool_fun_fun$ 0)
+(declare-sort Enat_enat_bool_fun_fun$ 0)
+(declare-sort Nat_bool_fun_nat_bool_fun_fun$ 0)
+(declare-datatypes ((Nat_option$ 0)(Enat$ 0)) (((none$) (some$ (the$ Nat$)))
+((abs_enat$ (rep_enat$ Nat_option$)))
+))
+(declare-sort A_stream$ 0)
+(declare-fun shd$ (A_stream$) A$)
+(declare-fun stl$ (A_stream$) A_stream$)
+(declare-fun sCons$ (A$ A_stream$) A_stream$)
+(declare-fun i$ () Nat$)
+(declare-fun p$ () A_stream_bool_fun$)
+(declare-fun ia$ () Nat$)
+(declare-fun uu$ (Nat$) Nat_bool_fun$)
+(declare-fun suc$ (Nat$) Nat$)
+(declare-fun uua$ (Enat$) Nat_bool_fun$)
+(declare-fun uub$ (Bool_bool_fun$) Nat_bool_fun_nat_bool_fun_fun$)
+(declare-fun uuc$ (Enat$) Nat_bool_fun$)
+(declare-fun uud$ () Nat_nat_fun$)
+(declare-fun eSuc$ (Enat$) Enat$)
+(declare-fun enat$ (Nat$) Enat$)
+(declare-fun less$ (Nat$) Nat_bool_fun$)
+(declare-fun plus$ (Enat$) Enat_enat_fun$)
+(declare-fun less$a (Enat$) Enat_bool_fun$)
+(declare-fun omega$ () A_stream$)
+(declare-fun plus$a (Nat$) Nat_nat_fun$)
+(declare-fun sdrop$ (Nat$ A_stream$) A_stream$)
+(declare-fun omega$a () A_stream$)
+(declare-fun sfirst$ (A_stream_bool_fun$ A_stream$) Enat$)
+(declare-fun fun_app$ (Nat_bool_fun$ Nat$) Bool)
+(declare-fun less_eq$ (Nat$) Nat_bool_fun$)
+(declare-fun case_nat$ (Bool) Nat_bool_fun_nat_bool_fun_fun$)
+(declare-fun fun_app$a (Enat_bool_fun$ Enat$) Bool)
+(declare-fun fun_app$b (Bool_enat_bool_fun_fun$ Bool) Enat_bool_fun$)
+(declare-fun fun_app$c (Nat_bool_fun_nat_bool_fun_fun$ Nat_bool_fun$) Nat_bool_fun$)
+(declare-fun fun_app$d (Bool_bool_fun$ Bool) Bool)
+(declare-fun fun_app$e (Nat_nat_fun$ Nat$) Nat$)
+(declare-fun fun_app$f (A_stream_bool_fun$ A_stream$) Bool)
+(declare-fun fun_app$g (Nat_enat_fun$ Nat$) Enat$)
+(declare-fun fun_app$h (Enat_enat_fun$ Enat$) Enat$)
+(declare-fun fun_app$i (Enat_nat_fun$ Enat$) Nat$)
+(declare-fun fun_app$j (Enat_enat_bool_fun_fun$ Enat$) Enat_bool_fun$)
+(declare-fun fun_app$k (Nat_nat_bool_fun_fun$ Nat$) Nat_bool_fun$)
+(declare-fun fun_app$l (Nat_bool_fun_nat_fun$ Nat_bool_fun$) Nat$)
+(declare-fun greatest$ (Enat_bool_fun$) Enat$)
+(declare-fun less_eq$a (Enat$) Enat_bool_fun$)
+(declare-fun rec_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$)
+(declare-fun case_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$)
+(declare-fun greatest$a () Nat_bool_fun_nat_fun$)
+(declare-fun greatestM$ (Nat_nat_fun$) Nat_bool_fun_nat_fun$)
+(assert (and
+(forall ((?v0 Nat$) (?v1 A_stream_bool_fun$) (?v2 A_stream$)) (=> (fun_app$a (less$a (enat$ ?v0)) (sfirst$ ?v1 ?v2)) (not (fun_app$f ?v1 (sdrop$ ?v0 ?v2)))) )
+(not (fun_app$a (less_eq$a (sfirst$ p$ omega$)) (enat$ (suc$ ia$))))
+(fun_app$f p$ (sdrop$ (suc$ ia$) omega$))
+(forall ((?v0 Enat$) (?v1 Enat$)) (=> (not (fun_app$a (less$a ?v0) ?v1)) (fun_app$a (less_eq$a ?v1) ?v0)) )
+))
+(check-sat)
+(exit)
--- /dev/null
+(set-logic AUFBVDTNIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-sort us_private 0)
+
+(declare-sort integer 0)
+
+(declare-fun to_rep1 (integer) Int)
+
+(declare-datatypes ()
+((us_split_fields
+ (mk___split_fields (rec__unit1__t1__c1 integer)(rec__ext__ us_private)))))
+
+(declare-datatypes ()
+((us_split_fields__ref
+ (mk___split_fields__ref (us_split_fields__content us_split_fields)))))
+(define-fun us_split_fields__ref___projection ((a us_split_fields__ref)) us_split_fields
+ (us_split_fields__content a))
+
+(declare-datatypes ()
+((us_rep (mk___rep (us_split_fields1 us_split_fields)(attr__tag Int)))))
+(define-fun us_rep___projection ((a us_rep)) us_split_fields (us_split_fields1
+ a))
+
+(declare-fun is_zero (us_rep) Bool)
+
+(declare-fun is_zero__post_predicate (Bool us_rep) Bool)
+
+;; is_zero__def_axiom
+ (assert
+ (forall ((x us_rep))
+ (! (=> (is_zero__post_predicate (is_zero x) x)
+ (= (= (is_zero x) true)
+ (= (to_rep1 (rec__unit1__t1__c1 (us_split_fields1 x))) 0))) :pattern (
+ (is_zero x)) )))
+
+(declare-datatypes ()
+((us_split_fields2
+ (mk___split_fields1
+ (rec__unit2__t2__c2 integer)(rec__unit1__t1__c11 integer)(rec__ext__1 us_private)))))
+
+(declare-datatypes ()
+((us_split_fields__ref1
+ (mk___split_fields__ref1 (us_split_fields__content1 us_split_fields2)))))
+(define-fun us_split_fields__ref_2__projection ((a us_split_fields__ref1)) us_split_fields2
+ (us_split_fields__content1 a))
+
+(declare-datatypes ()
+((us_rep1 (mk___rep1 (us_split_fields3 us_split_fields2)(attr__tag1 Int)))))
+(define-fun us_rep_3__projection ((a us_rep1)) us_split_fields2 (us_split_fields3
+ a))
+
+(declare-fun hide_ext__ (integer us_private) us_private)
+
+(define-fun to_base ((a us_rep1)) us_rep (mk___rep
+ (mk___split_fields
+ (rec__unit1__t1__c11
+ (us_split_fields3 a))
+ (hide_ext__
+ (rec__unit2__t2__c2
+ (us_split_fields3 a))
+ (rec__ext__1 (us_split_fields3 a))))
+ (attr__tag1 a)))
+
+(declare-fun is_zero2 (us_rep1) Bool)
+
+(declare-fun is_zero__post_predicate2 (Bool us_rep1) Bool)
+
+;; is_zero__def_axiom
+ (assert
+ (forall ((x us_rep1))
+ (! (=> (is_zero__post_predicate2 (is_zero2 x) x)
+ (= (= (is_zero2 x) true)
+ (and (= (is_zero (to_base x)) true)
+ (= (to_rep1 (rec__unit2__t2__c2 (us_split_fields3 x))) 0)))) :pattern (
+ (is_zero2 x)) )))
+
+(declare-fun x2__attr__tag () Int)
+
+(declare-fun x2__split_fields () integer)
+
+(declare-fun x2__split_fields1 () integer)
+
+(declare-fun x2__split_fields2 () us_private)
+
+;; H
+ (assert
+ (forall ((x2__split_fields3 us_split_fields2)) (is_zero__post_predicate2
+ (is_zero2 (mk___rep1 x2__split_fields3 x2__attr__tag))
+ (mk___rep1 x2__split_fields3 x2__attr__tag))))
+
+;; H
+ (assert
+ (and (= (to_rep1 x2__split_fields1) 0) (= (to_rep1 x2__split_fields) 0)))
+
+;; Should be enough to imply following hypothesis
+ (assert
+ (forall ((x us_rep1)) (is_zero__post_predicate (is_zero (to_base x))
+ (to_base x))))
+
+(assert
+;; WP_parameter_def
+ ;; File "main.adb", line 5, characters 0-0
+ (not
+ (= (is_zero (to_base (mk___rep1
+ (mk___split_fields1 x2__split_fields x2__split_fields1
+ x2__split_fields2) x2__attr__tag))) true)))
+(check-sat)
projects / cvc5.git / commitdiff