From c431410d0bd4a688d5d446f906d80634424dcd53 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Apr 2014 10:31:47 -0500 Subject: Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit. --- test/regress/regress0/bug512.smt2 | 2 +- .../regress0/fmf/Arrow_Order-smtlib.778341.smt | 2 +- test/regress/regress0/fmf/Makefile.am | 11 +++++-- test/regress/regress0/fmf/QEpres-uf.855035.smt | 2 +- test/regress/regress0/fmf/fc-pigeonhole19.smt2 | 20 +++++++++++++ test/regress/regress0/fmf/fc-simple.smt2 | 12 ++++++++ test/regress/regress0/fmf/fc-unsat-pent.smt2 | 20 +++++++++++++ test/regress/regress0/fmf/fc-unsat-tot-2.smt2 | 14 +++++++++ test/regress/regress0/quantifiers/bug269.smt2 | 2 ++ test/regress/regress0/quantifiers/burns13.smt2 | 2 ++ test/regress/regress0/rewriterules/Makefile.am | 6 ++-- test/regress/regress0/rewriterules/read5.smt2 | 35 ++++++++++++++++++++++ test/regress/regress0/tptp/Makefile.am | 2 +- 13 files changed, 120 insertions(+), 10 deletions(-) create mode 100755 test/regress/regress0/fmf/fc-pigeonhole19.smt2 create mode 100755 test/regress/regress0/fmf/fc-simple.smt2 create mode 100755 test/regress/regress0/fmf/fc-unsat-pent.smt2 create mode 100755 test/regress/regress0/fmf/fc-unsat-tot-2.smt2 create mode 100755 test/regress/regress0/rewriterules/read5.smt2 (limited to 'test/regress/regress0') diff --git a/test/regress/regress0/bug512.smt2 b/test/regress/regress0/bug512.smt2 index b0c970f37..1c8a0626a 100644 --- a/test/regress/regress0/bug512.smt2 +++ b/test/regress/regress0/bug512.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --tlimit-per 2500 -iq ; EXPECT: unknown -; EXPECT: (:reason-unknown timeout) +; EXPECT: (:reason-unknown incomplete) ; EXPECT: unsat (set-option :print-success false) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index 536bc241f..f62f057e4 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: unsat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b9a87231f..395054d67 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -23,18 +23,23 @@ TESTS = \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ - Hoare-z3.931718.smt \ QEpres-uf.855035.smt \ agree467.smt2 \ Arrow_Order-smtlib.778341.smt \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 \ - fmf-bound-int.smt2 + fmf-bound-int.smt2 \ + fc-simple.smt2 \ + fc-unsat-tot-2.smt2 \ + fc-unsat-pent.smt2 \ + fc-pigeonhole19.smt2 EXTRA_DIST = $(TESTS) +# disabled for now : +# Hoare-z3.931718.smt bug0909.smt2 + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 980e5fd49..2945c8f4d 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: sat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 new file mode 100755 index 000000000..15c36682c --- /dev/null +++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 @@ -0,0 +1,20 @@ +(set-logic UFC) +(set-info :status unsat) + +(declare-sort P 0) +(declare-sort H 0) + +(declare-fun p () P) +(declare-fun h () H) + +; pigeonhole using native cardinality constraints +(assert (fmf.card p 19)) +(assert (not (fmf.card p 18))) +(assert (fmf.card h 18)) +(assert (not (fmf.card h 17))) + +; each pigeon has different holes +(declare-fun f (P) H) +(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2)))))) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2 new file mode 100755 index 000000000..d1fd2301c --- /dev/null +++ b/test/regress/regress0/fmf/fc-simple.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun c () U) + +(assert (fmf.card c 2)) +(assert (not (fmf.card a 4))) + +(check-sat) diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2 new file mode 100755 index 000000000..f1721cb04 --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(declare-fun e () U) + +(assert (not (= a b))) +(assert (not (= b c))) +(assert (not (= c d))) +(assert (not (= d e))) +(assert (not (= e a))) + +(assert (fmf.card c 2)) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 new file mode 100755 index 000000000..d946974ed --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 @@ -0,0 +1,14 @@ +(set-logic UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) + +(assert (not (fmf.card a 2))) + +(assert (forall ((x U)) (or (= x a) (= x b)))) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/bug269.smt2 b/test/regress/regress0/quantifiers/bug269.smt2 index 0d5aedbb3..2e50030d1 100644 --- a/test/regress/regress0/quantifiers/bug269.smt2 +++ b/test/regress/regress0/quantifiers/bug269.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic LRA) (set-info :status unsat) (declare-fun x4 () Real) diff --git a/test/regress/regress0/quantifiers/burns13.smt2 b/test/regress/regress0/quantifiers/burns13.smt2 index ad970a2b2..3424c161e 100644 --- a/test/regress/regress0/quantifiers/burns13.smt2 +++ b/test/regress/regress0/quantifiers/burns13.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant --decision=internal +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 3a3a097bd..31f99905c 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -23,16 +23,16 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 \ - length_trick2.smt2 \ length_gen_020.smt2 \ datatypes.smt2 \ datatypes_sat.smt2 \ reachability_back_to_the_future.smt2 \ relation.smt2 \ simulate_rewriting.smt2 \ - native_arrays.smt2 + native_arrays.smt2 \ + read5.smt2 -# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 +# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress0/rewriterules/read5.smt2 new file mode 100755 index 000000000..e66df7c7e --- /dev/null +++ b/test/regress/regress0/rewriterules/read5.smt2 @@ -0,0 +1,35 @@ +(set-logic AUF) +(set-info :source | +Translated from old SVC processor verification benchmarks. Contact Clark +Barrett at barrett@cs.nyu.edu for more information. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index) +(declare-fun a () Index) +(declare-fun aaa () Index) +(declare-fun aa () Index) +(declare-fun S () Arr) +(declare-fun vvv () Element) +(declare-fun v () Element) +(declare-fun vv () Element) +(declare-fun bbb () Index) +(declare-fun www () Element) +(declare-fun bb () Index) +(declare-fun ww () Element) +(declare-fun b () Index) +(declare-fun w () Element) +(declare-fun SS () Arr) +(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false)))) +; rewrite rule definition of arrays theory +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat) +(exit) diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e0c8a2b48..e9274d2ee 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -35,7 +35,6 @@ TESTS = \ tff0.p \ tff0-arith.p \ ARI086$(equals)1.p \ - BOO003-4.p \ DAT001$(equals)1.p \ KRS018+1.p \ KRS063+1.p \ @@ -62,6 +61,7 @@ TEST_DEPS_DIST = \ EXTRA_DIST = $(TESTS) \ $(TEST_DEPS_DIST) \ BOO027-1.p \ + BOO003-4.p \ MGT031-1.p \ NLP114-1.p \ SYN075+1.p -- cgit v1.2.3 From 6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Apr 2014 15:50:56 -0500 Subject: Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms. --- src/parser/smt2/smt2.cpp | 1 + src/printer/cvc/cvc_printer.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 1 + src/smt/boolean_terms.cpp | 4 +- src/theory/datatypes/datatypes_rewriter.h | 4 +- src/theory/datatypes/kinds | 2 + src/theory/datatypes/theory_datatypes.cpp | 55 +++++++++++++++++++--- src/theory/datatypes/theory_datatypes.h | 3 ++ src/theory/datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/quantifiers/options_handlers.h | 23 ++++----- src/theory/quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/trigger.cpp | 2 +- src/theory/theory_model.cpp | 4 +- test/regress/regress0/datatypes/Makefile.am | 3 +- test/regress/regress0/datatypes/datatype1.cvc | 2 +- test/regress/regress0/datatypes/datatype3.cvc | 2 +- test/regress/regress0/datatypes/wrong-sel-simp.cvc | 2 +- 17 files changed, 80 insertions(+), 33 deletions(-) (limited to 'test/regress/regress0') diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 64b321613..e9e6ba857 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); + Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; case THEORY_STRINGS: diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4d784c383..63529c2a5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::APPLY_TESTER: toStream(op, n.getOperator(), depth, types, false); break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ea335f2e5..1250bc659 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 111324dfa..e46a76ed7 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -152,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); appctorb << (*dt2)[i].getConstructor(); for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); } Node appctor = appctorb; if(i == 0) { @@ -191,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { for(size_t j = 0; j < ctor.getNumArgs(); ++j) { TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType); } Node appctor = appctorb; if(i == 0) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 37a656555..8cb3fb4a2 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -88,7 +88,7 @@ public: const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst(); return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst().getField())]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { // These strange (half-tuple-converted) terms can be created by // the system if you have something like "foo.1" for a tuple @@ -118,7 +118,7 @@ public: Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions // where the selector doesn't match the constructor, diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index bb6fd4373..b222738ae 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -39,6 +39,7 @@ cardinality TESTER_TYPE \ parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application" parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application" +parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)" parameterized APPLY_TESTER TESTER_TYPE 1: "tester application" @@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \ typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule +typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index b00b4148d..0b0f5807c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -54,7 +54,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); } @@ -318,6 +318,47 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { flushPendingFacts(); } +Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { + switch( n.getKind() ){ + case kind::APPLY_SELECTOR: { + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + size_t selectorIndex = Datatype::cindexOf(selectorExpr); + const Datatype& dt = Datatype::datatypeOf(selectorExpr); + const DatatypeConstructor& c = dt[selectorIndex]; + Expr tester = c.getTester(); + Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); + tst = Rewriter::rewrite( tst ); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + Node n_ret; + if( tst==NodeManager::currentNM()->mkConst( 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() ) ); + } + Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); + if( tst==NodeManager::currentNM()->mkConst( false ) ){ + n_ret = sk; + }else{ + n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk ); + } + } + //n_ret = Rewriter::rewrite( n_ret ); + Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; + return n_ret; + } + break; + default: + return n; + break; + } + Unreachable(); +} + void TheoryDatatypes::presolve() { Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } @@ -332,7 +373,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst().getIndex()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst().getIndex()].getSelector()), in[0]); } else if(in.getKind() == kind::RECORD_SELECT) { TypeNode t = in[0].getType(); if(t.hasAttribute(expr::DatatypeRecordAttr())) { @@ -340,7 +381,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst().getField()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst().getField()].getSelector()), in[0]); } TypeNode t = in.getType(); @@ -404,7 +445,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { b << in[1]; Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl; } else { - b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]); + b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]); Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; } } @@ -848,7 +889,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::collapseSelector( Node s, Node c ) { - Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c ); + Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); Node rr = Rewriter::rewrite( r ); //if( r!=rr ){ //Node eq_exp = NodeManager::currentNM()->mkConst(true); @@ -1075,7 +1116,7 @@ void TheoryDatatypes::collectTerms( Node n ) { //eqc->d_selectors = true; } */ - }else if( n.getKind() == APPLY_SELECTOR ){ + }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){ //we must also record which selectors exist Debug("datatypes") << " Found selector " << n << endl; if (n.getType().isBoolean()) { @@ -1117,7 +1158,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, std::vector< Node > children; children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ - Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ); + Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); if( mkVar ){ TypeNode tn = nc.getType(); if( dt.isParametric() ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 3a29433f8..2a93878d0 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -166,6 +166,8 @@ private: std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending_merge; + /** expand definition skolem functions */ + std::map< Node, Node > d_exp_def_skolem; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -208,6 +210,7 @@ public: void check(Effort e); void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest &logicRequest, Node n); Node ppRewrite(TNode n); void presolve(); void addSharedTerm(TNode t); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 527d110e0..d08b511dd 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule { struct DatatypeSelectorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::APPLY_SELECTOR); + Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL ); TypeNode selType = n.getOperator().getType(check); Type t = selType[0].toType(); Assert( t.isDatatype() ); diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 164e9e643..b7e624a66 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -92,8 +92,8 @@ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ gen-ev \n\ -+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper.\n\ ++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper based on generalizing evaluations.\n\ \n\ fmc-interval \n\ + Same as default, but with intervals for models of integer functions.\n\ @@ -131,9 +131,6 @@ conflict \n\ partial \n\ + Apply QCF algorithm to instantiate heuristically as well. \n\ \n\ -partial \n\ -+ Apply QCF to instantiate heuristically as well. \n\ -\n\ mc \n\ + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ \n\ @@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "gen-ev") { + if(optarg == "gen-ev") { return MBQI_GEN_EVAL; - } else if(optarg == "none") { + } else if(optarg == "none") { return MBQI_NONE; - } else if(optarg == "instgen") { + } else if(optarg == "instgen") { return MBQI_INST_GEN; - } else if(optarg == "default" || optarg == "fmc") { + } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; - } else if(optarg == "fmc-interval") { + } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; - } else if(optarg == "interval") { + } else if(optarg == "interval") { return MBQI_INTERVAL; - } else if(optarg == "trust") { + } else if(optarg == "trust") { return MBQI_TRUST; - } else if(optarg == "help") { + } else if(optarg == "help") { puts(mbqiModeHelp.c_str()); exit(1); } else { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c0b318f23..e27d438be 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) { return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 6912c9e89..3de12b9c9 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ bool Trigger::isAtomicTrigger( Node n ){ return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 405fceb6f..f207bdb8e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); d_eeContext->push(); } @@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t bool TheoryEngineModelBuilder::isAssignable(TNode n) { - return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR); + return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL); } diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 84adb4f84..e8a8f16f5 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -31,7 +31,6 @@ TESTS = \ datatype0.cvc \ datatype1.cvc \ datatype2.cvc \ - datatype3.cvc \ datatype4.cvc \ datatype13.cvc \ empty_tuprec.cvc \ @@ -64,6 +63,8 @@ TESTS = \ FAILING_TESTS = \ datatype-dump.cvc +# takes a long time to build model on debug : datatype3.cvc + EXTRA_DIST = $(TESTS) if CVC4_BUILD_PROFILE_COMPETITION diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc index 5172eeb48..3934959f1 100644 --- a/test/regress/regress0/datatypes/datatype1.cvc +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc index 5f130b6ae..fff1a5dd7 100644 --- a/test/regress/regress0/datatypes/datatype3.cvc +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index 7455f809c..b0dbdc46e 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE nat = succ(pred : nat) | zero END; -- cgit v1.2.3 From 1138911e0af7c15a7b41a5d02ff3edab2c837449 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Apr 2014 15:36:28 -0500 Subject: Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve datatypes rewrite, make option for previous dt semantics. --- src/theory/datatypes/datatypes_rewriter.h | 66 ++++++++++++++-------------- src/theory/datatypes/options | 4 +- src/theory/datatypes/theory_datatypes.cpp | 10 +++-- src/theory/quantifiers/first_order_model.cpp | 15 ++++++- src/theory/quantifiers/full_model_check.cpp | 2 +- test/regress/regress0/fmf/Makefile.am | 5 ++- 6 files changed, 60 insertions(+), 42 deletions(-) (limited to 'test/regress/regress0') diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 8cb3fb4a2..99245ef69 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -138,26 +138,25 @@ public: << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); }else{ - if( options::dtRewriteErrorSel() ){ - Node gt; - if( in.getType().isSort() ){ - TypeEnumerator te(in.getType()); - gt = *te; - }else{ - gt = in.getType().mkGroundTerm(); - } - TypeNode gtt = gt.getType(); - //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); - if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); - } - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " - << in.getType().mkGroundTerm() << std::endl; - return RewriteResponse(REWRITE_DONE,gt ); + //typically should not be called + Node gt; + if( in.getType().isSort() ){ + TypeEnumerator te(in.getType()); + gt = *te; + }else{ + gt = in.getType().mkGroundTerm(); } + TypeNode gtt = gt.getType(); + //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); + if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << " to distinguished ground term " + << in.getType().mkGroundTerm() << std::endl; + return RewriteResponse(REWRITE_DONE,gt ); } } if(in.getKind() == kind::TUPLE_SELECT && @@ -204,11 +203,18 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } - if(in.getKind() == kind::EQUAL && - checkClash(in[0], in[1])) { - Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(false)); + if(in.getKind() == kind::EQUAL ) { + std::vector< Node > rew; + if( checkClash(in[0], in[1], rew) ){ + Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(false)); + }else if( rew.size()!=1 || rew[0]!=in ){ + Node nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + Trace("datatypes-rewrite") << "Rewrite equality to " << nn << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, nn ); + } } return RewriteResponse(REWRITE_DONE, in); @@ -222,7 +228,7 @@ public: static inline void init() {} static inline void shutdown() {} - static bool checkClash( Node n1, Node n2 ) { + static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { @@ -231,18 +237,14 @@ public: } else { Assert( n1.getNumChildren() == n2.getNumChildren() ); for( int i=0; i<(int)n1.getNumChildren(); i++ ) { - if( checkClash( n1[i], n2[i] ) ) { + if( checkClash( n1[i], n2[i], rew ) ) { return true; } } } - }else if( !isTermDatatype( n1 ) ){ - //also check for clashes between non-datatypes + }else{ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); - eq = Rewriter::rewrite( eq ); - if( eq==NodeManager::currentNM()->mkConst(false) ){ - return true; - } + rew.push_back( eq ); } return false; } diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index 1daa30981..fcf36648d 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -9,8 +9,8 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory # then we do not rewrite such a selector term to an arbitrary ground term. # For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then # cdr( nil ) has no set value. -expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true - disable rewriting incorrectly applied selectors to arbitrary ground term +expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false + rewrite incorrectly applied selectors to arbitrary ground term option dtForceAssignment /--dt-force-assignment bool :default false :read-write force the datatypes solver to give specific values to all datatypes terms before answering sat diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fc37c5417..4858d99db 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -327,15 +327,18 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { switch( n.getKind() ){ case kind::APPLY_SELECTOR: { - Node selector = n.getOperator(); - Expr selectorExpr = selector.toExpr(); + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + if( options::dtRewriteErrorSel() ){ + return sel; + }else{ size_t selectorIndex = Datatype::cindexOf(selectorExpr); const Datatype& dt = Datatype::datatypeOf(selectorExpr); const DatatypeConstructor& c = dt[selectorIndex]; Expr tester = c.getTester(); Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); tst = Rewriter::rewrite( tst ); - Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); Node n_ret; if( tst==NodeManager::currentNM()->mkConst( true ) ){ n_ret = sel; @@ -357,6 +360,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; return n_ret; } + } break; default: return n; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 54be11b44..d5c2b0e9d 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); Node curr; for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { - Node v = getRepresentative( d_models[op]->d_value[i] ); + Node v = d_models[op]->d_value[i]; + if( !hasTerm( v ) ){ + //can happen when the model basis term does not exist in ground assignment + TypeNode tn = v.getType(); + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ + //see full_model_check.cpp line 366 + v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; + }else{ + Assert( false ); + } + } + v = getRepresentative( v ); if( curr.isNull() ){ curr = v; }else{ @@ -664,7 +675,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { if( !isStar(cond[j][1]) ){ children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); } - }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground representatives of this type... + }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ Node c = getUsedRepresentative( cond[j] ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6c889781d..126b30b81 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n void FullModelChecker::doNegate( Def & dc ) { for (unsigned i=0; i