From ba99b080d20d521603635a1f0b57be1436eca731 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Aug 2018 17:34:00 -0500 Subject: [PATCH] Fix inference of pre and post conditions for non variable arguments. (#2237) --- .../sygus/ce_guided_single_inv.cpp | 78 ++++++++++++++----- .../quantifiers/sygus/ce_guided_single_inv.h | 24 +++++- test/regress/Makefile.tests | 1 + .../quantifiers/horn-ground-pre-post.smt2 | 14 ++++ 4 files changed, 95 insertions(+), 22 deletions(-) create mode 100644 test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 9a6fad52a..6a7eb8197 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -770,6 +770,7 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st } void TransitionInference::process( Node n ) { + NodeManager* nm = NodeManager::currentNM(); d_complete = true; std::vector< Node > n_check; if( n.getKind()==AND ){ @@ -787,28 +788,29 @@ void TransitionInference::process( Node n ) { Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn << std::endl; if( processDisjunct( nn, terms, disjuncts, visited, true ) ){ if( !terms.empty() ){ - Node norm_args; + Node curr; int comp_num; std::map< bool, Node >::iterator itt = terms.find( false ); if( itt!=terms.end() ){ - norm_args = itt->second; + curr = itt->second; if( terms.find( true )!=terms.end() ){ comp_num = 0; }else{ comp_num = -1; } }else{ - norm_args = terms[true]; + curr = terms[true]; comp_num = 1; } - std::vector< Node > subs; - for( unsigned j=0; j vars; + std::vector svars; + getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts); for( unsigned j=0; j const_var; @@ -817,23 +819,32 @@ void TransitionInference::process( Node n ) { //transition Assert( terms.find( true )!=terms.end() ); Node next = terms[true]; - next = Rewriter::rewrite( next.substitute( subs.begin(), subs.end(), d_vars.begin(), d_vars.end() ) ); + next = Rewriter::rewrite(next.substitute( + vars.begin(), vars.end(), svars.begin(), svars.end())); Trace("cegqi-inv-debug") << "transition next predicate : " << next << std::endl; - // normalize the other direction - std::vector< Node > rvars; - for( unsigned i=0; imkSkolem( "ir", next[i].getType(), "template inference rev argument" ); + // make the primed variables if we have not already + if (d_prime_vars.empty()) + { + for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; + j++) + { + Node v = nm->mkSkolem( + "ir", next[j].getType(), "template inference rev argument"); d_prime_vars.push_back( v ); } } + // normalize the other direction Trace("cegqi-inv-debug2") << " normalize based on " << next << std::endl; - Assert( d_vars.size()==subs.size() ); + std::vector rvars; + std::vector rsvars; + getNormalizedSubstitution( + next, d_prime_vars, rvars, rsvars, disjuncts); + Assert(rvars.size() == rsvars.size()); for( unsigned j=0; j& pvars, + std::vector& vars, + std::vector& subs, + std::vector& disjuncts) +{ + for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++) + { + if (curr[j].getKind() == BOUND_VARIABLE) + { + // if the argument is a bound variable, add to the renaming + vars.push_back(curr[j]); + subs.push_back(pvars[j]); + } + else + { + // otherwise, treat as a constraint on the variable + // For example, this transforms e.g. a precondition clause + // I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ). + Node eq = curr[j].eqNode(pvars[j]); + disjuncts.push_back(eq.negate()); + } + } +} bool TransitionInference::processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, std::map< Node, bool >& visited, bool topLevel ) { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index b368a0689..00b50a4a1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -64,7 +64,29 @@ private: bool processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, std::map< Node, bool >& visited, bool topLevel ); void getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol ); bool d_complete; -public: + /** get normalized substitution + * + * This method takes as input a node curr of the form I( t1, ..., tn ) and + * a vector of variables pvars, where pvars.size()=n. For each ti that is + * a variable, it adds ti to vars, and pvars[i] to subs. For each ti that is + * not a variable, it adds the disequality ti != pvars[i] to disjuncts. + * + * This function is used for instance to normalize an arbitrary application of + * I so that is over arguments pvars. For instance if curr is I(3,5,y) and + * pvars = { x1,x2,x3 }, then the formula: + * I(3,5,y) ^ P(y) + * is equivalent to: + * x1 != 3 V x2 != 5 V I(x1,x2,x3) V P( y ) { y -> x3 } + * Here, we add y and x3 to vars and subs respectively, and x1!=3 and x2!=5 + * to disjuncts. + */ + void getNormalizedSubstitution(Node curr, + const std::vector& pvars, + std::vector& vars, + std::vector& subs, + std::vector& disjuncts); + + public: TransitionInference() : d_complete( false ) {} std::vector< Node > d_vars; std::vector< Node > d_prime_vars; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index aec72993c..2be59087b 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -606,6 +606,7 @@ REG0_TESTS = \ regress0/quantifiers/ex3.smt2 \ regress0/quantifiers/ex6.smt2 \ regress0/quantifiers/floor.smt2 \ + regress0/quantifiers/horn-ground-pre-post.smt2 \ regress0/quantifiers/is-even-pred.smt2 \ regress0/quantifiers/is-int.smt2 \ regress0/quantifiers/issue1805.smt2 \ diff --git a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 new file mode 100644 index 000000000..082df249b --- /dev/null +++ b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-inference +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) + +(declare-fun I (Int Int) Bool) + +(assert (I 1 0)) + +(assert (forall ((x Int) (y Int) (xp Int) (yp Int)) (=> (and (I x y) (= xp (+ x 1)) (= yp y)) (I xp yp)))) + +(assert (not (I 1 1))) + +(check-sat) -- 2.30.2