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> >());
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;
}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;
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 );
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;
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 );
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;
}
}
+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;
}
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 );
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 );
+ }
+ }
+}
+
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;
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 );
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 );
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
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");
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
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");
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,
* 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
* Datatype must be resolved.
*/
Expr getTester() const;
+
+ /** get sygus op */
+ Expr getSygusOp() const;
/**
* Get the tester name for this Datatype constructor.
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
*/
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();
/** 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
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);
}
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
# put it below in "TESTS +="
-TESTS =
+TESTS = hd-01-d1-prog.sy \
+ icfp_28_10.sy \
+ commutative.sy \
+ constant.sy \
+ multi-fun-polynomial2.sy \
+ unbdd_inv_gen_winf1.sy
# sygus tests currently taking too long for make regress
EXTRA_DIST = $(TESTS) \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun comm ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (comm x y) (comm y x)))
+
+
+(check-synth)
+
+; (+ x y) is a valid solution
\ No newline at end of file
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun constant ((x Int)) Int
+ ((Start Int (x
+ 0
+ 1
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (constant x) (constant y)))
+
+
+(check-synth)
+
+; 0, 1, (- x x) are valid solutions
\ No newline at end of file
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic BV)
+
+(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001)))
+
+(synth-fun f ((x (BitVec 32))) (BitVec 32)
+ ((Start (BitVec 32) ((bvand Start Start)
+ (bvsub Start Start)
+ (bvor Start Start)
+ (bvadd Start Start)
+ (bvxor Start Start)
+ x
+ #x00000000
+ #xFFFFFFFF
+ #x00000001))))
+
+(declare-var x (BitVec 32))
+(constraint (= (hd01 x) (f x)))
+(check-synth)
+
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic BV)
+
+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)
+ ))
+)
+)
+
+
+(constraint (= (f #xd74594057974e439) #x0000d74594057974))
+(constraint (= (f #x74641ebeee92e8a2) #x000074641ebeee92))
+(constraint (= (f #x91c80141d7ec76b1) #x000091c80141d7ec))
+(constraint (= (f #xe4e55862e5ee4bec) #x0000e4e55862e5ee))
+(constraint (= (f #x367da67ede4260ce) #x0000367da67ede42))
+(constraint (= (f #xa365eb36246b3d8e) #x0000a365eb36246b))
+(constraint (= (f #xcd8a44a6d4c09c29) #x0000cd8a44a6d4c0))
+(constraint (= (f #xa97e9b9b7970433d) #x0000a97e9b9b7970))
+(constraint (= (f #x474dec0dd75d6894) #x0000474dec0dd75d))
+(constraint (= (f #x12430014ed058b24) #x000012430014ed05))
+(check-synth)
; EXPECT: unsat
+; COMMAND-LINE: --cegqi
(set-logic LIA)
(synth-fun max ((x Int) (y Int)) Int
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun addExpr1 ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ 0
+ 1
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+(synth-fun addExpr2 ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ 0
+ 1
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x y)))
+
+
+(check-synth)
+
+; (x, y), (x-y, 0) ... are valid solutions
\ No newline at end of file
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+(synth-fun inv ((x Int)) Bool
+ (
+ (Start Bool ((and AtomicFormula AtomicFormula)
+ (or AtomicFormula AtomicFormula)))
+ (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
+ (Sum Int ((+ Term Term)))
+ (Term Int ((* Sign Var)))
+ (Sign Int (0 1 -1))
+ (Var Int (x))
+ (Const Int ((+ Const Const) (- Const Const) 0 1))
+ )
+)
+
+(define-fun implies ((b1 Bool) (b2 Bool)) Bool (or (not b1) b2))
+(define-fun and3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (and (and b1 b2) b3))
+(define-fun and4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (and (and3 b1 b2 b3) b4))
+(define-fun and5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (and (and4 b1 b2 b3 b4) b5))
+(define-fun and6 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool) (b6 Bool)) Bool (and (and5 b1 b2 b3 b4 b5) b6))
+(define-fun or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (or b1 b2) b3))
+(define-fun or4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (or (or3 b1 b2 b3) b4))
+(define-fun or5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (or (or4 b1 b2 b3 b4) b5))
+
+(declare-var s Int)
+
+(declare-var x Int)
+
+(constraint (implies (= x 0) (inv x)))
+(constraint (implies (inv x) (= x 0)))
+(constraint (implies (inv x) (inv x)))
+(constraint (implies (and (inv x) false) (not (= x 0))))
+
+(check-synth)
projects / cvc5.git / commitdiff