From c11154240248592b5446f1de4743d78ed2fb97bd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Aug 2019 14:44:14 -0500 Subject: [PATCH] Document transition inference utility (#3207) --- src/CMakeLists.txt | 2 + .../sygus/ce_guided_single_inv.cpp | 454 +------------- .../quantifiers/sygus/ce_guided_single_inv.h | 120 +--- .../sygus/transition_inference.cpp | 579 ++++++++++++++++++ .../quantifiers/sygus/transition_inference.h | 324 ++++++++++ 5 files changed, 913 insertions(+), 566 deletions(-) create mode 100644 src/theory/quantifiers/sygus/transition_inference.cpp create mode 100644 src/theory/quantifiers/sygus/transition_inference.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 16feace50..c75e5576f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -591,6 +591,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/synth_engine.h theory/quantifiers/sygus/term_database_sygus.cpp theory/quantifiers/sygus/term_database_sygus.h + theory/quantifiers/sygus/transition_inference.cpp + theory/quantifiers/sygus/transition_inference.h theory/quantifiers/sygus_sampler.cpp theory/quantifiers/sygus_sampler.h theory/quantifiers/term_database.cpp diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index a6eed127b..4289fc815 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -14,7 +14,6 @@ **/ #include "theory/quantifiers/sygus/ce_guided_single_inv.h" -#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -146,19 +145,18 @@ void CegSingleInv::initialize(Node q) Trace("cegqi-si") << "- Do transition inference..." << std::endl; d_ti[q].process(qq); Trace("cegqi-inv") << std::endl; - if (d_ti[q].d_func.isNull()) + Node prog = d_ti[q].getFunction(); + if (prog.isNull()) { // the invariant could not be inferred return; } NodeManager* nm = NodeManager::currentNM(); // map the program back via non-single invocation map - Node prog = d_ti[q].d_func; std::vector prog_templ_vars; - prog_templ_vars.insert( - prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end()); - d_trans_pre[prog] = d_ti[q].getComponent(1); - d_trans_post[prog] = d_ti[q].getComponent(-1); + d_ti[q].getVariables(prog_templ_vars); + d_trans_pre[prog] = d_ti[q].getPreCondition(); + d_trans_post[prog] = d_ti[q].getPostCondition(); Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; std::vector sivars; @@ -604,447 +602,5 @@ Node CegSingleInv::reconstructToSyntax(Node s, } void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; } - -bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){ - if( index==val.size() ){ - if( d_children.empty() ){ - d_children[loc].clear(); - return true; - }else{ - return false; - } - }else{ - return d_children[val[index]].add( loc, val, index+1 ); - } -} - -Node DetTrace::DetTraceTrie::constructFormula( std::vector< Node >& vars, unsigned index ){ - if( index==vars.size() ){ - return NodeManager::currentNM()->mkConst( true ); - }else{ - std::vector< Node > disj; - for( std::map< Node, DetTraceTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ - Node eq = vars[index].eqNode( it->first ); - if( indexsecond.constructFormula( vars, index+1 ); - disj.push_back( NodeManager::currentNM()->mkNode( kind::AND, eq, conc ) ); - }else{ - disj.push_back( eq ); - } - } - Assert( !disj.empty() ); - return disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); - } -} - -bool DetTrace::increment( Node loc, std::vector< Node >& vals ){ - if( d_trie.add( loc, vals ) ){ - for( unsigned i=0; i& vars ) { - return d_trie.constructFormula( vars ); -} - - -void DetTrace::print( const char* c ) { - for( unsigned i=0; i& vars ) { - Assert( d_vars.empty() ); - d_func = f; - d_vars.insert( d_vars.end(), vars.begin(), vars.end() ); -} - - -void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol ) { - for( unsigned j=0; j msum; - if (ArithMSum::getMonomialSumLit(slit, msum)) - { - for (std::map::iterator itm = msum.begin(); - itm != msum.end(); - ++itm) - { - if (std::find(vars.begin(), vars.end(), itm->first) != vars.end()) - { - Node veq_c; - Node val; - int ires = - ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); - if (ires != 0 && veq_c.isNull() - && !expr::hasSubterm(val, itm->first)) - { - v = itm->first; - s = val; - } - } - } - } - } - if( !v.isNull() ){ - TNode ts = s; - for( unsigned k=0; k " << s << std::endl; - const_var.push_back( v ); - const_subs.push_back( s ); - } - } - } -} - -void TransitionInference::process( Node n ) { - NodeManager* nm = NodeManager::currentNM(); - d_complete = true; - std::vector< Node > n_check; - if( n.getKind()==AND ){ - for( unsigned i=0; i > visited; - std::map< bool, Node > terms; - std::vector< Node > disjuncts; - Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn << std::endl; - if( processDisjunct( nn, terms, disjuncts, visited, true ) ){ - if( !terms.empty() ){ - Node curr; - int comp_num; - std::map< bool, Node >::iterator itt = terms.find( false ); - if( itt!=terms.end() ){ - curr = itt->second; - if( terms.find( true )!=terms.end() ){ - comp_num = 0; - }else{ - comp_num = -1; - } - }else{ - curr = terms[true]; - comp_num = 1; - } - Trace("cegqi-inv-debug2") - << " normalize based on " << curr << std::endl; - std::vector vars; - std::vector svars; - getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts); - for( unsigned j=0; j const_var; - std::vector< Node > const_subs; - if( comp_num==0 ){ - //transition - Assert( terms.find( true )!=terms.end() ); - Node next = terms[true]; - next = Rewriter::rewrite(next.substitute( - vars.begin(), vars.end(), svars.begin(), svars.end())); - Trace("cegqi-inv-debug") << "transition next predicate : " << next << std::endl; - // 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; - std::vector rvars; - std::vector rsvars; - getNormalizedSubstitution( - next, d_prime_vars, rvars, rsvars, disjuncts); - Assert(rvars.size() == rsvars.size()); - for( unsigned j=0; jmkConst( false ); - }else if( disjuncts.size()==1 ){ - res = disjuncts[0]; - }else{ - res = NodeManager::currentNM()->mkNode( kind::OR, disjuncts ); - } - if (!expr::hasBoundVar(res)) - { - Trace("cegqi-inv") << "*** inferred " << ( comp_num==1 ? "pre" : ( comp_num==-1 ? "post" : "trans" ) ) << "-condition : " << res << std::endl; - d_com[comp_num].d_conjuncts.push_back( res ); - if( !const_var.empty() ){ - bool has_const_eq = const_var.size()==d_vars.size(); - Trace("cegqi-inv") << " with constant substitution, complete = " << has_const_eq << " : " << std::endl; - for( unsigned i=0; i " << const_subs[i] << std::endl; - if( has_const_eq ){ - d_com[comp_num].d_const_eq[res][const_var[i]] = const_subs[i]; - } - } - Trace("cegqi-inv") << "...size = " << const_var.size() << ", #vars = " << d_vars.size() << std::endl; - } - }else{ - Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl; - d_complete = false; - } - } - }else{ - d_complete = false; - } - } - - // finalize the components - for( int i=-1; i<=1; i++ ){ - Node ret; - if( d_com[i].d_conjuncts.empty() ){ - ret = NodeManager::currentNM()->mkConst( true ); - }else if( d_com[i].d_conjuncts.size()==1 ){ - ret = d_com[i].d_conjuncts[0]; - }else{ - ret = NodeManager::currentNM()->mkNode( kind::AND, d_com[i].d_conjuncts ); - } - if( i==0 || i==1 ){ - // pre-condition and transition are negated - ret = TermUtil::simpleNegate( ret ); - } - d_com[i].d_this = ret; - } -} -void TransitionInference::getNormalizedSubstitution( - Node curr, - const std::vector& 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& terms, - std::vector& disjuncts, - std::map >& visited, - bool topLevel) -{ - if (visited[topLevel].find(n) == visited[topLevel].end()) - { - visited[topLevel][n] = true; - bool childTopLevel = n.getKind()==OR && topLevel; - //if another part mentions UF or a free variable, then fail - bool lit_pol = n.getKind()!=NOT; - Node lit = n.getKind()==NOT ? n[0] : n; - if( lit.getKind()==APPLY_UF ){ - Node op = lit.getOperator(); - if( d_func.isNull() ){ - d_func = op; - Trace("cegqi-inv-debug") << "Use " << op << " with args "; - for( unsigned i=0; imkSkolem( "i", lit[i].getType(), "template inference argument" ); - d_vars.push_back( v ); - Trace("cegqi-inv-debug") << v << " "; - } - Trace("cegqi-inv-debug") << std::endl; - } - if( op!=d_func ){ - Trace("cegqi-inv-debug") << "...failed, free function : " << n << std::endl; - return false; - }else if( topLevel ){ - if( terms.find( lit_pol )==terms.end() ){ - terms[lit_pol] = lit; - return true; - }else{ - Trace("cegqi-inv-debug") << "...failed, repeated inv-app : " << lit << std::endl; - return false; - } - }else{ - Trace("cegqi-inv-debug") << "...failed, non-entailed inv-app : " << lit << std::endl; - return false; - } - }else if( topLevel && !childTopLevel ){ - disjuncts.push_back( n ); - } - for( unsigned i=0; i >::iterator it = d_com[index].d_const_eq.find( loc ); - if( it!=d_com[index].d_const_eq.end() ){ - std::vector< Node > next; - for( unsigned i=0; isecond.find( v )!=it->second.end() ); - next.push_back( it->second[v] ); - dt.d_curr.push_back( it->second[v] ); - } - Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl; - bool ret = dt.increment( loc, next ); - AlwaysAssert( ret ); - return 0; - } - return -1; -} - -int TransitionInference::incrementTrace( DetTrace& dt, Node loc, bool fwd ) { - Assert( d_com[0].has( loc ) ); - // check if it satisfies the pre/post condition - int check_index = fwd ? -1 : 1; - Node cc = getComponent( check_index ); - Assert( !cc.isNull() ); - Node ccr = Rewriter::rewrite( cc.substitute( d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end() ) ); - if( ccr.isConst() ){ - if( ccr.getConst()==( fwd ? false : true ) ){ - Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl; - return 2; - } - } - - - // terminates? - Node c = getComponent( 0 ); - Assert( !c.isNull() ); - - Assert( d_vars.size()==dt.d_curr.size() ); - Node cr = Rewriter::rewrite( c.substitute( d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end() ) ); - if( cr.isConst() ){ - if( !cr.getConst() ){ - Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl; - return 1; - }else{ - return -1; - } - } - if( fwd ){ - Component& cm = d_com[0]; - std::map >::iterator it = - cm.d_const_eq.find(loc); - if (it != cm.d_const_eq.end()) - { - std::vector< Node > next; - for( unsigned i=0; isecond.find( pv )!=it->second.end() ); - Node pvs = it->second[pv]; - Assert( d_vars.size()==dt.d_curr.size() ); - Node pvsr = Rewriter::rewrite( pvs.substitute( d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end() ) ); - next.push_back( pvsr ); - } - if( dt.increment( loc, next ) ){ - Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl; - return 0; - }else{ - // looped - Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl; - return 1; - } - } - }else{ - //TODO - } - return -1; -} - -int TransitionInference::initializeTrace( DetTrace& dt, bool fwd ) { - Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl; - int index = fwd ? 1 : -1; - if( d_com[index].d_conjuncts.size()==1 ){ - return initializeTrace( dt, d_com[index].d_conjuncts[0], fwd ); - }else{ - return -1; - } -} - -int TransitionInference::incrementTrace( DetTrace& dt, bool fwd ) { - if( d_com[0].d_conjuncts.size()==1 ){ - return incrementTrace( dt, d_com[0].d_conjuncts[0], fwd ); - }else{ - return -1; - } -} - -Node TransitionInference::constructFormulaTrace( DetTrace& dt ) { - return dt.constructFormula( d_vars ); -} } //namespace CVC4 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index fb216ce0b..00e3639f8 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -18,10 +18,11 @@ #define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #include "context/cdlist.h" -#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" -#include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/single_inv_partition.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/sygus/transition_inference.h" namespace CVC4 { namespace theory { @@ -29,121 +30,6 @@ namespace quantifiers { class SynthConjecture; -class DetTrace { -private: - class DetTraceTrie { - public: - std::map< Node, DetTraceTrie > d_children; - bool add( Node loc, std::vector< Node >& val, unsigned index = 0 ); - void clear() { d_children.clear(); } - Node constructFormula( std::vector< Node >& vars, unsigned index = 0 ); - }; - DetTraceTrie d_trie; -public: - std::vector< Node > d_curr; - bool increment( Node loc, std::vector< Node >& vals ); - Node constructFormula( std::vector< Node >& vars ); - void print( const char* c ); -}; - -/** - * This class is used for inferring that an arbitrary synthesis conjecture - * corresponds to an invariant synthesis problem for some predicate (d_func). - * - * The invariant-to-synthesize can either be explicitly given, via a call - * to initialize( f, vars ), or otherwise inferred if this method is not called. - */ -class TransitionInference { - private: - /** process disjunct - * - * The purpose of this function is to infer pre/post/transition conditions - * for a (possibly unknown) invariant-to-synthesis, given a conjunct from - * an arbitrary synthesis conjecture. - * - * Assume our negated synthesis conjecture is of the form: - * forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n})) - * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true - * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i} - * to disjuncts. - * - * If this method returns true, then (1) all applications of free function - * symbols have operator d_func. Note this function may set d_func to a - * function symbol in n if d_func was null prior to this call. In other words, - * this method may infer the subject of the invariant synthesis problem; - * (2) all occurrences of d_func are "top-level", that is, each Fij may be - * of the form (not) ( tj ), but otherwise d_func does not occur in - * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of - * ( tj ), and (not ( tk )). - * - * If the above conditions are met, then terms[true] is set to ( tj ) - * if Fij is ( tj ) for some j, and likewise terms[false] - * is set to ( tk ) if Fik is (not ( tk )) for some k. - * - * The argument visited caches the results of this function for (topLevel, n). - */ - bool processDisjunct(Node n, - std::map& terms, - std::vector& disjuncts, - std::map >& 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; - /** 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; - /** - * The function (predicate) that is the subject of the invariant synthesis - * problem we are inferring. - */ - Node d_func; - - class Component { - public: - Component(){} - Node d_this; - std::vector< Node > d_conjuncts; - std::map< Node, std::map< Node, Node > > d_const_eq; - bool has( Node c ) { return std::find( d_conjuncts.begin(), d_conjuncts.end(), c )!=d_conjuncts.end(); } - }; - std::map< int, Component > d_com; - - void initialize( Node f, std::vector< Node >& vars ); - void process( Node n ); - Node getComponent( int i ); - bool isComplete() { return d_complete; } - - // 0 : success, 1 : terminated, 2 : counterexample, -1 : invalid - int initializeTrace( DetTrace& dt, Node loc, bool fwd = true ); - int incrementTrace( DetTrace& dt, Node loc, bool fwd = true ); - int initializeTrace( DetTrace& dt, bool fwd = true ); - int incrementTrace( DetTrace& dt, bool fwd = true ); - Node constructFormulaTrace( DetTrace& dt ); -}; - // this class infers whether a conjecture is single invocation (Reynolds et al CAV 2015), and sets up the // counterexample-guided quantifier instantiation utility (d_cinst), and methods for solution // reconstruction (d_sol). diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp new file mode 100644 index 000000000..88ffe84b2 --- /dev/null +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -0,0 +1,579 @@ +/********************* */ +/*! \file transition_inference.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implmentation of utility for inferring whether a synthesis conjecture + ** encodes a transition system. + ** + **/ +#include "theory/quantifiers/sygus/transition_inference.h" + +#include "expr/node_algorithm.h" +#include "theory/arith/arith_msum.h" +#include "theory/quantifiers/term_util.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +bool DetTrace::DetTraceTrie::add(Node loc, const std::vector& val) +{ + DetTraceTrie* curr = this; + for (const Node& v : val) + { + curr = &(curr->d_children[v]); + } + if (curr->d_children.empty()) + { + curr->d_children[loc].clear(); + return true; + } + return false; +} + +Node DetTrace::DetTraceTrie::constructFormula(const std::vector& vars, + unsigned index) +{ + NodeManager* nm = NodeManager::currentNM(); + if (index == vars.size()) + { + return nm->mkConst(true); + } + std::vector disj; + for (std::pair& p : d_children) + { + Node eq = vars[index].eqNode(p.first); + if (index < vars.size() - 1) + { + Node conc = p.second.constructFormula(vars, index + 1); + disj.push_back(nm->mkNode(AND, eq, conc)); + } + else + { + disj.push_back(eq); + } + } + Assert(!disj.empty()); + return disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); +} + +bool DetTrace::increment(Node loc, std::vector& vals) +{ + if (d_trie.add(loc, vals)) + { + for (unsigned i = 0, vsize = vals.size(); i < vsize; i++) + { + d_curr[i] = vals[i]; + } + return true; + } + return false; +} + +Node DetTrace::constructFormula(const std::vector& vars) +{ + return d_trie.constructFormula(vars); +} + +void DetTrace::print(const char* c) const +{ + for (const Node& n : d_curr) + { + Trace(c) << n << " "; + } +} + +Node TransitionInference::getFunction() const { return d_func; } + +void TransitionInference::getVariables(std::vector& vars) const +{ + vars.insert(vars.end(), d_vars.begin(), d_vars.end()); +} + +Node TransitionInference::getPreCondition() const { return d_pre.d_this; } +Node TransitionInference::getPostCondition() const { return d_post.d_this; } +Node TransitionInference::getTransitionRelation() const +{ + return d_trans.d_this; +} + +void TransitionInference::getConstantSubstitution( + const std::vector& vars, + const std::vector& disjuncts, + std::vector& const_var, + std::vector& const_subs, + bool reqPol) +{ + for (const Node& d : disjuncts) + { + Node sn; + if (!const_var.empty()) + { + sn = d.substitute(const_var.begin(), + const_var.end(), + const_subs.begin(), + const_subs.end()); + sn = Rewriter::rewrite(sn); + } + else + { + sn = d; + } + bool slit_pol = sn.getKind() != NOT; + Node slit = sn.getKind() == NOT ? sn[0] : sn; + if (slit.getKind() == EQUAL && slit_pol == reqPol) + { + // check if it is a variable equality + TNode v; + Node s; + for (unsigned r = 0; r < 2; r++) + { + if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end()) + { + if (!expr::hasSubterm(slit[1 - r], slit[r])) + { + v = slit[r]; + s = slit[1 - r]; + break; + } + } + } + if (v.isNull()) + { + // solve for var + std::map msum; + if (ArithMSum::getMonomialSumLit(slit, msum)) + { + for (std::pair& m : msum) + { + if (std::find(vars.begin(), vars.end(), m.first) != vars.end()) + { + Node veq_c; + Node val; + int ires = ArithMSum::isolate(m.first, msum, veq_c, val, EQUAL); + if (ires != 0 && veq_c.isNull() + && !expr::hasSubterm(val, m.first)) + { + v = m.first; + s = val; + } + } + } + } + } + if (!v.isNull()) + { + TNode ts = s; + for (unsigned k = 0, csize = const_subs.size(); k < csize; k++) + { + const_subs[k] = Rewriter::rewrite(const_subs[k].substitute(v, ts)); + } + Trace("cegqi-inv-debug2") + << "...substitution : " << v << " -> " << s << std::endl; + const_var.push_back(v); + const_subs.push_back(s); + } + } + } +} + +void TransitionInference::process(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + d_complete = true; + std::vector n_check; + if (n.getKind() == AND) + { + for (const Node& nc : n) + { + n_check.push_back(nc); + } + } + else + { + n_check.push_back(n); + } + for (const Node& nn : n_check) + { + std::map > visited; + std::map terms; + std::vector disjuncts; + Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn + << std::endl; + if (!processDisjunct(nn, terms, disjuncts, visited, true)) + { + d_complete = false; + continue; + } + if (terms.empty()) + { + continue; + } + Node curr; + // The component that this disjunct contributes to, where + // 1 : pre-condition, -1 : post-condition, 0 : transition relation + int comp_num; + std::map::iterator itt = terms.find(false); + if (itt != terms.end()) + { + curr = itt->second; + if (terms.find(true) != terms.end()) + { + comp_num = 0; + } + else + { + comp_num = -1; + } + } + else + { + curr = terms[true]; + comp_num = 1; + } + Trace("cegqi-inv-debug2") << " normalize based on " << curr << std::endl; + std::vector vars; + std::vector svars; + getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts); + for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++) + { + Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl; + disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute( + vars.begin(), vars.end(), svars.begin(), svars.end())); + Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl; + } + std::vector const_var; + std::vector const_subs; + if (comp_num == 0) + { + // transition + Assert(terms.find(true) != terms.end()); + Node next = terms[true]; + next = Rewriter::rewrite(next.substitute( + vars.begin(), vars.end(), svars.begin(), svars.end())); + Trace("cegqi-inv-debug") + << "transition next predicate : " << next << std::endl; + // 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; + std::vector rvars; + std::vector rsvars; + getNormalizedSubstitution(next, d_prime_vars, rvars, rsvars, disjuncts); + Assert(rvars.size() == rsvars.size()); + for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++) + { + Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl; + disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute( + rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end())); + Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl; + } + getConstantSubstitution( + d_prime_vars, disjuncts, const_var, const_subs, false); + } + else + { + getConstantSubstitution(d_vars, disjuncts, const_var, const_subs, false); + } + Node res; + if (disjuncts.empty()) + { + res = nm->mkConst(false); + } + else if (disjuncts.size() == 1) + { + res = disjuncts[0]; + } + else + { + res = nm->mkNode(OR, disjuncts); + } + if (expr::hasBoundVar(res)) + { + Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl; + d_complete = false; + continue; + } + Trace("cegqi-inv") << "*** inferred " + << (comp_num == 1 ? "pre" + : (comp_num == -1 ? "post" : "trans")) + << "-condition : " << res << std::endl; + Component& c = + (comp_num == 1 ? d_pre : (comp_num == -1 ? d_post : d_trans)); + c.d_conjuncts.push_back(res); + if (!const_var.empty()) + { + bool has_const_eq = const_var.size() == d_vars.size(); + Trace("cegqi-inv") << " with constant substitution, complete = " + << has_const_eq << " : " << std::endl; + for (unsigned i = 0, csize = const_var.size(); i < csize; i++) + { + Trace("cegqi-inv") << " " << const_var[i] << " -> " + << const_subs[i] << std::endl; + if (has_const_eq) + { + c.d_const_eq[res][const_var[i]] = const_subs[i]; + } + } + Trace("cegqi-inv") << "...size = " << const_var.size() + << ", #vars = " << d_vars.size() << std::endl; + } + } + + // finalize the components + for (int i = -1; i <= 1; i++) + { + Component& c = (i == 1 ? d_pre : (i == -1 ? d_post : d_trans)); + Node ret; + if (c.d_conjuncts.empty()) + { + ret = nm->mkConst(true); + } + else if (c.d_conjuncts.size() == 1) + { + ret = c.d_conjuncts[0]; + } + else + { + ret = nm->mkNode(AND, c.d_conjuncts); + } + if (i == 0 || i == 1) + { + // pre-condition and transition are negated + ret = TermUtil::simpleNegate(ret); + } + c.d_this = ret; + } +} +void TransitionInference::getNormalizedSubstitution( + Node curr, + const std::vector& 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& terms, + std::vector& disjuncts, + std::map >& visited, + bool topLevel) +{ + if (visited[topLevel].find(n) != visited[topLevel].end()) + { + return true; + } + visited[topLevel][n] = true; + bool childTopLevel = n.getKind() == OR && topLevel; + // if another part mentions UF or a free variable, then fail + bool lit_pol = n.getKind() != NOT; + Node lit = n.getKind() == NOT ? n[0] : n; + if (lit.getKind() == APPLY_UF) + { + Node op = lit.getOperator(); + if (d_func.isNull()) + { + d_func = op; + Trace("cegqi-inv-debug") << "Use " << op << " with args "; + NodeManager* nm = NodeManager::currentNM(); + for (const Node& l : lit) + { + Node v = nm->mkSkolem("i", l.getType(), "template inference argument"); + d_vars.push_back(v); + Trace("cegqi-inv-debug") << v << " "; + } + Trace("cegqi-inv-debug") << std::endl; + } + if (op != d_func) + { + Trace("cegqi-inv-debug") + << "...failed, free function : " << n << std::endl; + return false; + } + else if (topLevel) + { + if (terms.find(lit_pol) == terms.end()) + { + terms[lit_pol] = lit; + return true; + } + else + { + Trace("cegqi-inv-debug") + << "...failed, repeated inv-app : " << lit << std::endl; + return false; + } + } + Trace("cegqi-inv-debug") + << "...failed, non-entailed inv-app : " << lit << std::endl; + return false; + } + else if (topLevel && !childTopLevel) + { + disjuncts.push_back(n); + } + for (const Node& nc : n) + { + if (!processDisjunct(nc, terms, disjuncts, visited, childTopLevel)) + { + return false; + } + } + return true; +} + +TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt, + Node loc, + bool fwd) +{ + Component& c = fwd ? d_pre : d_post; + Assert(c.has(loc)); + std::map >::iterator it = c.d_const_eq.find(loc); + if (it != c.d_const_eq.end()) + { + std::vector next; + for (const Node& v : d_vars) + { + Assert(it->second.find(v) != it->second.end()); + next.push_back(it->second[v]); + dt.d_curr.push_back(it->second[v]); + } + Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl; + bool ret = dt.increment(loc, next); + AlwaysAssert(ret); + return TRACE_INC_SUCCESS; + } + return TRACE_INC_INVALID; +} + +TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt, + Node loc, + bool fwd) +{ + Assert(d_trans.has(loc)); + // check if it satisfies the pre/post condition + Node cc = fwd ? getPostCondition() : getPreCondition(); + Assert(!cc.isNull()); + Node ccr = Rewriter::rewrite(cc.substitute( + d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end())); + if (ccr.isConst()) + { + if (ccr.getConst() == (fwd ? false : true)) + { + Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl; + return TRACE_INC_CEX; + } + } + + // terminates? + Node c = getTransitionRelation(); + Assert(!c.isNull()); + + Assert(d_vars.size() == dt.d_curr.size()); + Node cr = Rewriter::rewrite(c.substitute( + d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end())); + if (cr.isConst()) + { + if (!cr.getConst()) + { + Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl; + return TRACE_INC_TERMINATE; + } + return TRACE_INC_INVALID; + } + if (!fwd) + { + // only implemented in forward direction + Assert(false); + return TRACE_INC_INVALID; + } + Component& cm = d_trans; + std::map >::iterator it = cm.d_const_eq.find(loc); + if (it == cm.d_const_eq.end()) + { + return TRACE_INC_INVALID; + } + std::vector next; + for (const Node& pv : d_prime_vars) + { + Assert(it->second.find(pv) != it->second.end()); + Node pvs = it->second[pv]; + Assert(d_vars.size() == dt.d_curr.size()); + Node pvsr = Rewriter::rewrite(pvs.substitute( + d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end())); + next.push_back(pvsr); + } + if (dt.increment(loc, next)) + { + Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl; + return TRACE_INC_SUCCESS; + } + // looped + Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl; + return TRACE_INC_TERMINATE; +} + +TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt, bool fwd) +{ + Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl; + Component& c = fwd ? d_pre : d_post; + if (c.d_conjuncts.size() == 1) + { + return initializeTrace(dt, c.d_conjuncts[0], fwd); + } + return TRACE_INC_INVALID; +} + +TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt, bool fwd) +{ + if (d_trans.d_conjuncts.size() == 1) + { + return incrementTrace(dt, d_trans.d_conjuncts[0], fwd); + } + return TRACE_INC_INVALID; +} + +Node TransitionInference::constructFormulaTrace(DetTrace& dt) const +{ + return dt.constructFormula(d_vars); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h new file mode 100644 index 000000000..b4fb220db --- /dev/null +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -0,0 +1,324 @@ +/********************* */ +/*! \file transition_inference.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Utility for inferring whether a synthesis conjecture encodes a + ** transition system. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H +#define CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H + +#include +#include + +#include "expr/node.h" + +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/inst_match_trie.h" +#include "theory/quantifiers/single_inv_partition.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * Utility for storing a deterministic trace of a transition system. A trace + * is stored as a collection of vectors of values that have been taken by + * the variables of transition system. For example, say we have a transition + * system with variables x,y,z. Say the precondition constrains these variables + * to x=1,y=2,z=3, and say that the transition relation admits the single + * trace: [1,2,3], [2,3,4], [3,4,5]. We store these three vectors of variables + * in the trie within this class. + * + * This utility is used for determining whether a transition system has a + * deterministic terminating trace and hence a trivial invariant. + */ +class DetTrace +{ + public: + /** The current value of the trace */ + std::vector d_curr; + /** + * Increment the trace: index the current values, if successful (they are + * not a duplicate of a previous value), update the current values to vals. + * Returns true if the increment was successful. + */ + bool increment(Node loc, std::vector& vals); + /** + * Construct the formula that this trace represents with respect to variables + * in vars. For details, see DetTraceTrie::constructFormula below. + */ + Node constructFormula(const std::vector& vars); + /** Debug print this trace on trace message c */ + void print(const char* c) const; + + private: + /** + * A trie of value vectors for the variables of a transition system. Nodes + * are stored as data in tries with no children at the leaves of this trie. + */ + class DetTraceTrie + { + public: + /** the children of this trie */ + std::map d_children; + /** Add data loc to this trie, indexed by val. */ + bool add(Node loc, const std::vector& val); + /** clear the trie */ + void clear() { d_children.clear(); } + /** + * Construct the formula corresponding to this trie with respect to + * variables in vars. For example, if we have indexed [1,2,3] and [2,3,4] + * and vars is [x,y,z], then this method returns: + * ( x=1 ^ y=2 ^ z=3 ) V ( x=2 ^ y=3 ^ z=4 ). + */ + Node constructFormula(const std::vector& vars, unsigned index = 0); + }; + /** The above trie data structure for this class */ + DetTraceTrie d_trie; +}; + +/** + * Trace increment status, used for incrementTrace below. + */ +enum TraceIncStatus +{ + // the trace was successfully incremented to a new value + TRACE_INC_SUCCESS, + // the trace terminated + TRACE_INC_TERMINATE, + // the trace encountered a bad state (violating the post-condition) + TRACE_INC_CEX, + // the trace was invalid + TRACE_INC_INVALID +}; + +/** + * This class is used for inferring that an arbitrary synthesis conjecture + * corresponds to an invariant synthesis problem for some predicate (d_func). + * + * The invariant-to-synthesize can either be explicitly given, via a call + * to initialize( f, vars ), or otherwise inferred if this method is not called. + */ +class TransitionInference +{ + public: + TransitionInference() : d_complete(false) {} + /** Process the conjecture n + * + * This initializes this class with information related to viewing it as a + * transition system. This means we infer a function, the state variables, + * the pre/post condition and transition relation. + * + * The node n should be the inner body of the negated synthesis conjecture, + * prior to generating the deep embedding. That is, given: + * forall f. ~forall x. P( f, x ), + * this method expects n to be P( f, x ). + */ + void process(Node n); + /** + * Get the function that is the subject of the synthesis problem we are + * analyzing. + */ + Node getFunction() const; + /** + * Get the variables that the function is applied to. These are the free + * variables of the pre/post condition, and transition relation. These are + * fresh (Skolem) variables allocated by this class. + */ + void getVariables(std::vector& vars) const; + /** + * Get the pre/post condition, or transition relation that was inferred by + * this class. + */ + Node getPreCondition() const; + Node getPostCondition() const; + Node getTransitionRelation() const; + /** + * Was the analysis of the conjecture complete? + * + * If this is false, then the system we have inferred does not take into + * account all of the synthesis conjecture. This is the case when process(...) + * was called on formula that does not have the shape of a transition system. + */ + bool isComplete() const { return d_complete; } + + /** + * The following two functions are used for computing whether this transition + * relation is deterministic and terminating. + * + * The argument fwd is whether we are going in the forward direction of the + * transition system (starting from the precondition). + * + * If fwd is true, the initializeTrace method returns TRACE_INC_SUCCESS if the + * precondition consists of a single conjunct of the form + * ( x1 = t1 ^ ... ^ xn = tn ) + * where x1...xn are the state variables of the transition system. Otherwise + * it returns TRACE_INC_INVALID. + */ + TraceIncStatus initializeTrace(DetTrace& dt, bool fwd = true); + /** + * Increment the trace dt in direction fwd. + * + * If fwd is true, the incrementTrace method returns TRACE_INC_INVALID if the + * transition relation is not of the form + * ( x1' = t1[X] ^ ... ^ xn' = tn[X] ^ Q[X] ^ P(x1...xn) ) => P( x1'...xn' ) + * Otherwise, it returns TRACE_INC_TERMINATE if the values of + * x1' = t1[dt.d_curr] ^ ... ^ xn' = tn[dt.d_curr] have already been executed + * on trace dt (the trace has looped), or if + * x1' = t1[dt.d_curr] ^ ... ^ xn' = tn[dt.d_curr] ^ Q[dt.d_curr] is unsat + * (the trace has terminated). It returns TRACE_INC_CEX if the postcondition + * is false for the values t1[dt.d_curr] ^ ... ^ tn[dt.d_curr]. Otherwise, + * it returns TRACE_INC_SUCCESS. + */ + TraceIncStatus incrementTrace(DetTrace& dt, bool fwd = true); + /** + * Constructs the formula corresponding to trace dt with respect to the + * variables of this class. + */ + Node constructFormulaTrace(DetTrace& dt) const; + + private: + /** + * The function (predicate) that is the subject of the invariant synthesis + * problem we are inferring. + */ + Node d_func; + /** The variables that the function is applied to */ + std::vector d_vars; + /** + * The variables that the function is applied to in the next state of the + * inferred transition relation. + */ + std::vector d_prime_vars; + /** + * Was the analysis of the synthesis conjecture passed to the process method + * of this class complete? + */ + bool d_complete; + + /** process disjunct + * + * The purpose of this function is to infer pre/post/transition conditions + * for a (possibly unknown) invariant-to-synthesis, given a conjunct from + * an arbitrary synthesis conjecture. + * + * Assume our negated synthesis conjecture is of the form: + * forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n})) + * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true + * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i} + * to disjuncts. + * + * If this method returns true, then (1) all applications of free function + * symbols have operator d_func. Note this function may set d_func to a + * function symbol in n if d_func was null prior to this call. In other words, + * this method may infer the subject of the invariant synthesis problem; + * (2) all occurrences of d_func are "top-level", that is, each Fij may be + * of the form (not) ( tj ), but otherwise d_func does not occur in + * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of + * ( tj ), and (not ( tk )). + * + * If the above conditions are met, then terms[true] is set to ( tj ) + * if Fij is ( tj ) for some j, and likewise terms[false] + * is set to ( tk ) if Fik is (not ( tk )) for some k. + * + * The argument visited caches the results of this function for (topLevel, n). + */ + bool processDisjunct(Node n, + std::map& terms, + std::vector& disjuncts, + std::map >& visited, + bool topLevel); + /** + * This method infers if the conjunction of disjuncts is equivalent to a + * conjunction of the form + * (~) const_var[1] = const_subs[1] ... (~) const_var[n] = const_subs[n] + * where the above equalities are negated iff reqPol is false, and + * const_var[1] ... const_var[n] + * are distinct members of vars + */ + void getConstantSubstitution(const std::vector& vars, + const std::vector& disjuncts, + std::vector& const_var, + std::vector& const_subs, + bool reqPol); + /** 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); + /** + * Stores one of the components of the inferred form of the synthesis + * conjecture (precondition, postcondition, or transition relation). + */ + class Component + { + public: + Component() {} + /** The formula that was inferred for this component */ + Node d_this; + /** The list of conjuncts of the above formula */ + std::vector d_conjuncts; + /** + * Maps formulas to the constant equality substitution that it entails. + * For example, the formula (x=4 ^ y=x+5) may map to { x -> 4, y -> 9 }. + */ + std::map > d_const_eq; + /** Does this component have conjunct c? */ + bool has(Node c) const + { + return std::find(d_conjuncts.begin(), d_conjuncts.end(), c) + != d_conjuncts.end(); + } + }; + /** Components for the pre/post condition and transition relation. */ + Component d_pre; + Component d_post; + Component d_trans; + /** + * Initialize trace dt, loc is a node to identify the trace, fwd is whether + * we are going in the forward direction of the transition system (starting + * from the precondition). + * + * The argument loc is a conjunct of transition relation that entails that the + * trace dt has executed in its last step to its current value. For example, + * if the transition relation is ( x'=x+1 ^ P( x ) ) => P(x'), and our trace's + * current value was last updated [x:=1] -> [x:=2] based on x'=x+1, then loc + * is the node x'=x+1. + */ + TraceIncStatus initializeTrace(DetTrace& dt, Node loc, bool fwd = true); + /** Same as above, for incrementing the trace dt */ + TraceIncStatus incrementTrace(DetTrace& dt, Node loc, bool fwd = true); +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif -- 2.30.2