From a50f977b02c5653e03d4f3d9d8c7df1f9e2be48e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 20 Jan 2015 14:23:04 +0100 Subject: [PATCH] Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions. --- src/parser/smt2/Smt2.g | 1 + src/parser/smt2/smt2.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 81 +++++++++++++++---- src/theory/datatypes/theory_datatypes.h | 6 ++ src/theory/quantifiers/options | 2 + src/util/datatype.cpp | 22 +++++ src/util/datatype.h | 17 ++++ test/regress/regress0/sygus/Makefile.am | 7 +- test/regress/regress0/sygus/commutative.sy | 22 +++++ test/regress/regress0/sygus/constant.sy | 23 ++++++ test/regress/regress0/sygus/hd-01-d1-prog.sy | 22 +++++ test/regress/regress0/sygus/icfp_28_10.sy | 40 +++++++++ test/regress/regress0/sygus/max.sl | 1 + .../regress0/sygus/multi-fun-polynomial2.sy | 35 ++++++++ .../regress0/sygus/unbdd_inv_gen_winf1.sy | 36 +++++++++ 15 files changed, 300 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress0/sygus/commutative.sy create mode 100644 test/regress/regress0/sygus/constant.sy create mode 100644 test/regress/regress0/sygus/hd-01-d1-prog.sy create mode 100644 test/regress/regress0/sygus/icfp_28_10.sy create mode 100644 test/regress/regress0/sygus/multi-fun-polynomial2.sy create mode 100644 test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy 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()); cnames.push_back(std::vector()); cargs.push_back(std::vector >()); 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& 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 children; - for( unsigned i=0; imkNode( 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 d_args; + /** the operator associated with this constructor (for sygus) */ + Expr d_sygus_op; void resolve(ExprManager* em, DatatypeType self, const std::map& 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); } diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index ad1296af0..b5ea8b476 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -18,7 +18,12 @@ MAKEFLAGS = -k # 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) \ diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy new file mode 100644 index 000000000..15567b0a8 --- /dev/null +++ b/test/regress/regress0/sygus/commutative.sy @@ -0,0 +1,22 @@ +; 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 diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy new file mode 100644 index 000000000..ddc12a6a9 --- /dev/null +++ b/test/regress/regress0/sygus/constant.sy @@ -0,0 +1,23 @@ +; 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 diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy new file mode 100644 index 000000000..a58bc2f64 --- /dev/null +++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy @@ -0,0 +1,22 @@ +; 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) + diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy new file mode 100644 index 000000000..6e1610337 --- /dev/null +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -0,0 +1,40 @@ +; 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) diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sl index aea8e8186..fdd925196 100644 --- a/test/regress/regress0/sygus/max.sl +++ b/test/regress/regress0/sygus/max.sl @@ -1,4 +1,5 @@ ; EXPECT: unsat +; COMMAND-LINE: --cegqi (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy new file mode 100644 index 000000000..24d49ee4e --- /dev/null +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -0,0 +1,35 @@ +; 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 diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy new file mode 100644 index 000000000..dc39efd84 --- /dev/null +++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy @@ -0,0 +1,36 @@ +; 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) -- 2.30.2