diff options
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 7 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/error1-dt.sy | 71 |
4 files changed, 85 insertions, 11 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9b34b1d7c..163c8acad 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1476,18 +1476,15 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const return; } } + Node p = n.getAttribute(theory::SygusPrintProxyAttribute()); + if (!p.isNull()) + { + out << p; + } else { - Node p = n.getAttribute(theory::SygusPrintProxyAttribute()); - if (!p.isNull()) - { - out << p; - } - else - { - // cannot convert term to analog, print original - out << n; - } + // cannot convert term to analog, print original + out << n; } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 01d08dad8..af8c93e45 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -874,8 +874,13 @@ void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, un // do not recurse to non-datatype types return; } + const Datatype& dt = tn.getDatatype(); + if( !dt.isSygus() ) + { + // do not recurse to non-sygus datatype types + return; + } d_min_type_depth[root_tn][tn] = type_depth; - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); //compute for connected types for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index af6a9b839..29f31960c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1641,6 +1641,7 @@ set(regress_1_tests regress1/sygus/double.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy + regress1/sygus/error1-dt.sy regress1/sygus/extract.sy regress1/sygus/fg_polynomial3.sy regress1/sygus/find_sc_bvult_bvnot.sy diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy new file mode 100644 index 000000000..67f73aded --- /dev/null +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -0,0 +1,71 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-active-gen=enum + +(set-logic ALL_SUPPORTED) + +(declare-datatypes ((IntRange 0)) + (((IntRange (lower Int) (upper Int))))) + +(declare-datatypes ((Loc 0)) + (((Loc (x Int) (y Int))))) + +(declare-datatypes ((LocRange 0)) + (((LocRange (xD IntRange) (yD IntRange))))) + +(declare-datatypes ((Ship 0)) + (((Ship (shipCapacity Int) (shipLoc Loc))))) + +(declare-datatypes ((ShipRange 0)) + (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange))))) + +(define-fun betweenInt ((x Int) (r IntRange)) Bool + (and (< (lower r) x) (< x (upper r))) +) + +(define-fun betweenLoc ((l Loc) (lr LocRange)) Bool + (and (betweenInt (x l) (xD lr)) (betweenInt (y l) (yD lr))) +) + +(define-fun subsetInt ((r1 IntRange) (r2 IntRange)) Bool + (and (>= (lower r1) (lower r2)) (<= (upper r1) (upper r2))) +) + +(define-fun betweenShip ((s Ship) (sr ShipRange)) Bool + (and (betweenInt (shipCapacity s) (shipCapacityD sr)) (betweenLoc (shipLoc s) (shipLocD sr))) +) + +(define-fun atLeast ((s Ship)) Bool + (> (shipCapacity s) 50) +) + +(define-fun subsetLoc ((s1 LocRange) (s2 LocRange)) Bool + (and (subsetInt (xD s1) (xD s2)) (subsetInt (yD s1) (yD s2))) +) + +(define-fun subsetShip ((s1 ShipRange) (s2 ShipRange)) Bool + (and (subsetInt (shipCapacityD s1) (shipCapacityD s2)) (subsetLoc (shipLocD s1) (shipLocD s2))) +) + +(define-fun max ((x Int) (y Int)) Int + (ite (>= x y) x y) +) + +(define-fun min ((x Int) (y Int)) Int + (ite (<= x y) x y) +) + + +(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange) + +(declare-var secret Ship) +(declare-var prior ShipRange) +(declare-var response Bool) + +(constraint + (=> (betweenShip secret (f secret prior response)) + (= response + (and (atLeast secret) + (subsetShip (f secret prior response) prior)))) +) + +(check-synth) |