diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
commit | a50f977b02c5653e03d4f3d9d8c7df1f9e2be48e (patch) | |
tree | 9e8c569a9250c6c8c7eb7826539e63ae414133d9 /src | |
parent | 9e5b1fd1083c1c82d5bbc61a4a316211db629c43 (diff) |
Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 1 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 81 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rw-r--r-- | src/util/datatype.cpp | 22 | ||||
-rw-r--r-- | src/util/datatype.h | 17 |
7 files changed, 115 insertions, 16 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d2f38cc82..a83299d3b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -600,6 +600,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::string dname = ss.str(); sorts.push_back(t); datatypes.push_back(Datatype(dname)); + datatypes.back().setSygusType( t ); ops.push_back(std::vector<Expr>()); cnames.push_back(std::vector<std::string>()); cargs.push_back(std::vector<std::vector<CVC4::Type> >()); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 077f385b0..c6c3a896c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -534,7 +534,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, testerId.append(name); checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); + CVC4::DatatypeConstructor c(name, testerId, ops[i] ); for( unsigned j=0; j<cargs[i].size(); j++ ){ std::stringstream sname; sname << name << "_" << j; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index bf986a138..8db9435ed 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -238,11 +238,16 @@ void TheoryDatatypes::check(Effort e) { }else{ Trace("dt-split") << "*************Split for constructors on " << n << endl; std::vector< Node > children; - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - Node test = DatatypesRewriter::mkTester( n, i, dt ); - children.push_back( test ); + if( dt.isSygus() && options::sygusNormalForm() ){ + getSygusSplits( n, dt, children ); + }else{ + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + Node test = DatatypesRewriter::mkTester( n, i, dt ); + children.push_back( test ); + } } - Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children ); + Assert( !children.empty() ); + Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children ); d_out->lemma( lemma ); } return; @@ -294,10 +299,10 @@ void TheoryDatatypes::flushPendingFacts(){ Node exp = d_pending_exp[ fact ]; //check to see if we have to communicate it to the rest of the system if( mustCommunicateFact( fact, exp ) ){ - Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl; + Trace("dt-lemma-debug") << "Assert fact " << fact << " with explanation " << exp << std::endl; Node lem = fact; if( exp.isNull() || exp==d_true ){ - lem = fact; + Trace("dt-lemma-debug") << "Trivial explanation." << std::endl; }else{ Trace("dt-lemma-debug") << "Get explanation..." << std::endl; Node ee_exp = explain( exp ); @@ -394,12 +399,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { if( tst==d_true ){ n_ret = sel; }else{ - if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){ - std::stringstream ss; - ss << selector << "_uf"; - d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), - NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) ); - } + mkExpDefSkolem( selector, n[0].getType(), n.getType() ); Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); if( tst==NodeManager::currentNM()->mkConst( false ) ){ n_ret = sk; @@ -694,7 +694,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( !cons1.isNull() && !cons2.isNull() ){ Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl; Node unifEq = cons1.eqNode( cons2 ); -#if 0 + /* std::vector< Node > exp; std::vector< std::pair< TNode, TNode > > deq_cand; bool conf = checkClashModEq( cons1, cons2, exp, deq_cand ); @@ -711,11 +711,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( conf ){ exp.push_back( unifEq ); d_conflictNode = explain( exp ); -#else + */ std::vector< Node > rew; if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ d_conflictNode = explain( unifEq ); -#endif Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; @@ -864,6 +863,15 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > } } +void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) { + if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){ + std::stringstream ss; + ss << sel << "_uf"; + d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), + NodeManager::currentNM()->mkFunctionType( dt, rt ) ); + } +} + void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl; Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; @@ -1032,8 +1040,15 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::collapseSelector( Node s, Node c ) { + Assert( c.getKind()==APPLY_CONSTRUCTOR ); + Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl; Node r; if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){ + //Trace("dt-collapse-sel") << "Indices : " << Datatype::indexOf(c.getOperator().toExpr()) << " " << Datatype::cindexOf(s.getOperator().toExpr()) << std::endl; + //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){ + // mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() ); + // r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] ); + //}else{ r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); }else if( s.getKind()==kind::DT_SIZE ){ r = NodeManager::currentNM()->mkNode( kind::DT_SIZE, c ); @@ -1901,3 +1916,39 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& return false; } +void TheoryDatatypes::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) { + Assert( dt.isSygus() ); + Trace("sygus-split") << "Get sygus splits " << n << std::endl; + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + Node op = n.getOperator(); + std::map< Node, std::vector< bool > >::iterator it = d_sygus_splits.find( op ); + if( it==d_sygus_splits.end() ){ + Expr selectorExpr = op.toExpr(); + int csIndex = Datatype::cindexOf(selectorExpr); + int sIndex = Datatype::indexOf(selectorExpr); + Trace("sygus-split") << " Constructor, selector index : " << csIndex << " " << sIndex << std::endl; + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + Expr sop = dt[i].getSygusOp(); + Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) ); + Trace("sygus-split") << " Operator #" << i << " : " << sop << ", kind = " << sk << std::endl; + bool addSplit = true; + //TODO + + d_sygus_splits[op].push_back( addSplit ); + } + } + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + if( d_sygus_splits[op][i] ){ + Node test = DatatypesRewriter::mkTester( n, i, dt ); + splits.push_back( test ); + } + } + Assert( !splits.empty() ); + }else{ + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + Node test = DatatypesRewriter::mkTester( n, i, dt ); + splits.push_back( test ); + } + } +} + diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 30b0140a9..2f0ec20ec 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -133,6 +133,8 @@ private: bool hasTester( Node n ); /** get the possible constructors for n */ void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); + /** mkExpDefSkolem */ + void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ); private: /** The notify class */ NotifyClass d_notify; @@ -178,6 +180,8 @@ private: unsigned d_dtfCounter; /** expand definition skolem functions */ std::map< Node, Node > d_exp_def_skolem; + /** sygus splits */ + std::map< Node, std::vector< bool > > d_sygus_splits; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -276,6 +280,8 @@ private: bool mustCommunicateFact( Node n, Node exp ); /** check clash mod eq */ bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ); + /** get sygus splits */ + void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ); private: //equality queries bool hasTerm( TNode a ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index fc59b22b7..ad1508716 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -200,6 +200,8 @@ option sygusMinGrammar --sygus-min-grammar bool :default false minimize sygus grammars option sygusDecompose --sygus-decompose bool :default false decompose single invocation synthesis conjectures +option sygusNormalForm --sygus-normal-form bool :default true + only search for sygus builtin terms that are in normal form option localTheoryExt --local-t-ext bool :default false diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 7813626a7..c15e103f9 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -140,6 +140,14 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { d_constructors.push_back(c); } + +void Datatype::setSygusType( Type st ){ + CheckArgument(!d_resolved, this, + "cannot set sygus type to a finalized Datatype"); + d_sygus_type = st; +} + + Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); @@ -543,6 +551,15 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) : CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); } +DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) : + d_name(name + '\0' + tester), + d_tester(), + d_args(), + d_sygus_op(sygus_op) { + CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); + CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); +} + void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // We don't want to introduce a new data member, because eventually // we're going to be a constant stuffed inside a node. So we stow @@ -611,6 +628,11 @@ Expr DatatypeConstructor::getTester() const { return d_tester; } +Expr DatatypeConstructor::getSygusOp() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_op; +} + Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); diff --git a/src/util/datatype.h b/src/util/datatype.h index 32fae8235..084202956 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -185,6 +185,8 @@ private: Expr d_constructor; Expr d_tester; std::vector<DatatypeConstructorArg> d_args; + /** the operator associated with this constructor (for sygus) */ + Expr d_sygus_op; void resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, @@ -223,6 +225,7 @@ public: * constructor and tester aren't created until resolution time. */ DatatypeConstructor(std::string name, std::string tester); + DatatypeConstructor(std::string name, std::string tester, Expr sygus_op); /** * Add an argument (i.e., a data field) of the given name and type @@ -268,6 +271,9 @@ public: * Datatype must be resolved. */ Expr getTester() const; + + /** get sygus op */ + Expr getSygusOp() const; /** * Get the tester name for this Datatype constructor. @@ -453,6 +459,7 @@ private: bool d_resolved; Type d_self; bool d_involvesExt; + Type d_sygus_type; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -510,6 +517,9 @@ public: */ void addConstructor(const DatatypeConstructor& c); + /** set the sygus type of this datatype */ + void setSygusType( Type st ); + /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -530,6 +540,9 @@ public: /** is this a co-datatype? */ inline bool isCodatatype() const; + + /** is this a sygus datatype? */ + inline bool isSygus() const; /** * Return the cardinality of this datatype (the sum of the @@ -720,6 +733,10 @@ inline bool Datatype::isCodatatype() const { return d_isCo; } +inline bool Datatype::isSygus() const { + return !d_sygus_type.isNull(); +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } |