summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp109
-rw-r--r--src/theory/datatypes/datatypes_sygus.h44
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp29
-rw-r--r--src/theory/quantifiers/options6
4 files changed, 122 insertions, 66 deletions
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; i<children.size(); i++ ){
- Trace("sygus-split-debug3") << " " << children[i] << std::endl;
- }
- }
if( op.getKind()==BUILTIN ){
return NodeManager::currentNM()->mkNode( 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<Node> d_anchor;
- context::CDO<int> 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<Node> 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<int> 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<bool> 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback