From: ajreynol Date: Thu, 29 Jan 2015 09:17:58 +0000 (+0100) Subject: Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas. X-Git-Tag: cvc5-1.0.0~6417 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a8045f5f57c1e71dc4a2cdadc02ca09114c70af;p=cvc5.git Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas. --- diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 8bf3d4d64..62621f389 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -20,6 +20,7 @@ #include "expr/node_manager.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" +#include "smt/smt_engine_scope.h" #include "theory/quantifiers/options.h" @@ -739,31 +740,55 @@ bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) { SygusSymBreak::SygusSymBreak( SygusUtil * util, context::Context* c ) : -d_util( util ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_anchor( c ), d_prog_depth( c, 0 ), d_conflict( c ) { - +d_util( util ), d_context( c ) { } void SygusSymBreak::addTester( Node tst ) { + if( options::sygusNormalFormGlobal() ){ + Node a = getAnchor( tst[0] ); + Trace("sygus-sym-break-debug") << "Add tester " << tst << " for " << a << std::endl; + std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a ); + ProgSearch * ps; + if( it==d_prog_search.end() ){ + ps = new ProgSearch( this, a, d_context ); + d_prog_search[a] = ps; + }else{ + ps = it->second; + } + ps->addTester( tst ); + } +} + +Node SygusSymBreak::getAnchor( Node n ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + return getAnchor( n[0] ); + }else{ + return n; + } +} + +void SygusSymBreak::ProgSearch::addTester( Node tst ) { NodeMap::const_iterator it = d_testers.find( tst[0] ); if( it==d_testers.end() ){ d_testers[tst[0]] = tst; - if( d_anchor.get().isNull() ){ - if( tst[0].getKind()!=APPLY_SELECTOR_TOTAL ){ - d_anchor = tst[0]; - assignTester( tst, 0 ); - } + if( tst[0]==d_anchor ){ + assignTester( tst, 0 ); }else{ IntMap::const_iterator it = d_watched_terms.find( tst[0] ); if( it!=d_watched_terms.end() ){ assignTester( tst, (*it).second ); + }else{ + Trace("sygus-sym-break-debug2") << "...add to wait list " << tst << " for " << d_anchor << std::endl; } } + }else{ + Trace("sygus-sym-break-debug2") << "...already seen " << tst << " for " << d_anchor << std::endl; } } -void SygusSymBreak::assignTester( Node tst, int depth ) { - Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tst << ", depth = " << depth << std::endl; +void SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) { + Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tst << ", depth = " << depth << " of " << d_anchor << std::endl; int tindex = Datatype::indexOf( tst.getOperator().toExpr() ); TypeNode tn = tst[0].getType(); Assert( DatatypesRewriter::isTypeDatatype( tn ) ); @@ -786,7 +811,7 @@ void SygusSymBreak::assignTester( Node tst, int depth ) { }else{ d_watched_count[depth+1] = d_watched_count[depth+1] + dt[tindex].getNumArgs(); } - Trace("sygus-sym-break-debug") << "...watched count now " << d_watched_count[depth+1].get() << " for " << (depth+1) << std::endl; + Trace("sygus-sym-break-debug") << "...watched count now " << d_watched_count[depth+1].get() << " for " << (depth+1) << " of " << d_anchor << std::endl; //now decrement watch count and process if( depth>0 ){ Assert( d_watched_count[depth]>0 ); @@ -799,7 +824,7 @@ void SygusSymBreak::assignTester( Node tst, int depth ) { } } -Node SygusSymBreak::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) { +Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) { Assert( depth>=curr_depth ); Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl; NodeMap::const_iterator it = d_testers.find( prog ); @@ -818,10 +843,10 @@ Node SygusSymBreak::getCandidateProgramAtDepth( int depth, Node prog, int curr_d pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers ); } } - return d_util->mkGeneric( dt, tindex, var_count, pre ); + return d_parent->d_util->mkGeneric( dt, tindex, var_count, pre ); } -void SygusSymBreak::processProgramDepth( int depth ){ +void SygusSymBreak::ProgSearch::processProgramDepth( int depth ){ if( depth==d_prog_depth.get() && ( depth==0 || ( d_watched_count.find( depth )!=d_watched_count.end() && d_watched_count[depth]==0 ) ) ){ d_prog_depth = d_prog_depth + 1; if( depth>0 ){ @@ -829,32 +854,38 @@ void SygusSymBreak::processProgramDepth( int depth ){ std::map< TypeNode, int > var_count; std::vector< Node > testers; //now have entire information about candidate program at given depth - Node prog = getCandidateProgramAtDepth( depth, d_anchor.get(), 0, var_count, testers ); - if( d_normalized.find( prog )==d_normalized.end() ){ - Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << std::endl; - Node progr = Rewriter::rewrite( prog ); - std::map< TypeNode, int > var_count; - std::map< Node, Node > subs; - progr = d_util->getSygusNormalized( progr, var_count, subs ); - Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl; - d_normalized[prog] = progr; - std::map< Node, Node >::iterator it = d_normalized_to_orig.find( progr ); - if( it==d_normalized_to_orig.end() ){ - d_normalized_to_orig[progr] = prog; - }else{ - Assert( !testers.empty() ); - Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl; - Node conflict = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers ); - Trace("sygus-sym-break2") << "Conflict : " << conflict << std::endl; - } - } + Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, var_count, testers ); + d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers ); } processProgramDepth( depth+1 ); } } +void SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ) { + if( d_normalized[at].find( prog )==d_normalized[at].end() ){ + Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << " for " << a << std::endl; + Node progr = Rewriter::rewrite( prog ); + std::map< TypeNode, int > var_count; + std::map< Node, Node > subs; + progr = d_util->getSygusNormalized( progr, var_count, subs ); + Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl; + d_normalized[at][prog] = progr; + std::map< Node, Node >::iterator it = d_normalized_to_orig[at].find( progr ); + if( it==d_normalized_to_orig[at].end() ){ + d_normalized_to_orig[at][progr] = prog; + }else{ + Assert( !testers.empty() ); + Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl; + d_util->d_conflictNode = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers ); + Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl; + d_util->d_conflict = true; -SygusUtil::SygusUtil( Context* c ) { + // TODO : generalize conflict + } + } +} + +SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) { d_split = new SygusSplit( this ); d_sym_break = new SygusSymBreak( this, c ); } @@ -913,19 +944,17 @@ Node SygusUtil::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& Assert( !a.isNull() ); children.push_back( a ); } - if( Trace.isOn("sygus-split-debug3") ){ - Trace("sygus-split-debug3") << "mkGeneric " << dt[c].getName() << ", op = " << op << " with arguments : " << std::endl; - for( unsigned i=0; imkNode( op, children ); }else{ if( children.size()==1 ){ return children[0]; }else{ - return NodeManager::currentNM()->mkNode( APPLY, children ); + Node n = NodeManager::currentNM()->mkNode( APPLY, children ); + //must expand definitions + Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) ); + Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; + return ne; } } } diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 69806e076..fd0065667 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -110,22 +110,36 @@ public: class SygusSymBreak { - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; - typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; - typedef context::CDHashMap< int, int > IntIntMap; private: SygusUtil * d_util; - NodeMap d_testers; - IntMap d_watched_terms; - IntIntMap d_watched_count; - context::CDO d_anchor; - context::CDO d_prog_depth; - std::map< Node, Node > d_normalized; - std::map< Node, Node > d_normalized_to_orig; - void assignTester( Node tst, int depth ); - Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ); - void processProgramDepth( int depth ); - context::CDO d_conflict; + context::Context* d_context; + class ProgSearch { + typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; + typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; + typedef context::CDHashMap< int, int > IntIntMap; + private: + SygusSymBreak * d_parent; + Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ); + void processProgramDepth( int depth ); + void assignTester( Node tst, int depth ); + public: + ProgSearch( SygusSymBreak * p, Node a, context::Context* c ) : + d_parent( p ), d_anchor( a ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_prog_depth( c, 0 ) { + d_anchor_type = d_anchor.getType(); + } + Node d_anchor; + NodeMap d_testers; + IntMap d_watched_terms; + IntIntMap d_watched_count; + TypeNode d_anchor_type; + context::CDO d_prog_depth; + void addTester( Node tst ); + }; + std::map< Node, ProgSearch * > d_prog_search; + std::map< TypeNode, std::map< Node, Node > > d_normalized; + std::map< TypeNode, std::map< Node, Node > > d_normalized_to_orig; + Node getAnchor( Node n ); + void processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ); public: SygusSymBreak( SygusUtil * util, context::Context* c ); /** add tester */ @@ -150,6 +164,8 @@ public: SygusUtil( context::Context* c ); SygusSplit * getSplit() { return d_split; } SygusSymBreak * getSymBreak() { return d_sym_break; } + context::CDO d_conflict; + Node d_conflictNode; }; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f38545817..264158ed4 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -338,12 +338,14 @@ void TheoryDatatypes::flushPendingFacts(){ } void TheoryDatatypes::doPendingMerges(){ - //do all pending merges - int i=0; - while( i<(int)d_pending_merge.size() ){ - Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF ); - merge( d_pending_merge[i][0], d_pending_merge[i][1] ); - i++; + if( !d_conflict ){ + //do all pending merges + int i=0; + while( i<(int)d_pending_merge.size() ){ + Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF ); + merge( d_pending_merge[i][0], d_pending_merge[i][1] ); + i++; + } } d_pending_merge.clear(); } @@ -360,15 +362,22 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ doPendingMerges(); //add to tester if applicable if( atom.getKind()==kind::APPLY_TESTER ){ - if( polarity ){ + Node rep = getRepresentative( atom[0] ); + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + addTester( fact, eqc, rep ); + if( !d_conflict && polarity ){ Trace("dt-tester") << "Assert tester : " << atom << std::endl; if( d_sygus_util ){ d_sygus_util->getSymBreak()->addTester( atom ); + if( d_sygus_util->d_conflict ){ + d_conflict = true; + d_conflictNode = d_sygus_util->d_conflictNode; + Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + return; + } } } - Node rep = getRepresentative( atom[0] ); - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - addTester( fact, eqc, rep ); } doPendingMerges(); } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 6fc13498c..9d4281186 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,12 +196,14 @@ option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi -option sygusDecompose --sygus-decompose bool :default false - decompose single invocation synthesis conjectures +option sygusSingleInv --sygus-single-inv bool :default false + process single invocation synthesis conjectures option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form option sygusNormalFormArg --sygus-nf-arg bool :default true account for relationship between arguments of operations in sygus normal form +option sygusNormalFormGlobal --sygus-nf-global bool :default true + narrow sygus search space based on global state of current candidate program option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions