diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-10-07 16:41:13 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-10-07 16:41:13 -0400 |
commit | 1a56238b7ed75c6127293cb7c52d5b6b85245c64 (patch) | |
tree | e50005384d765b09853a52ecd712ed37a511979e | |
parent | 7d2265eb2b5dc96ddff04211959e208b1cb8a7f0 (diff) | |
parent | 2f716d8e5eaf4a75c2cf2e431b96ac1f3c9b8a5f (diff) |
merged golden
33 files changed, 2012 insertions, 663 deletions
diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf new file mode 100755 index 000000000..5df1f31c3 --- /dev/null +++ b/proofs/signatures/example.plf @@ -0,0 +1,116 @@ +; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+
+; --------------------------------------------------------------------------------
+; input :
+; ( a = b )
+; ( b = f(c) )
+; ( a != f(c) V a != b )
+
+; theory lemma (by transitivity) :
+; ( a != b V b != f(c) V a = f(c) )
+
+
+; With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+
+(check
+(% s sort
+(% a (term s)
+(% b (term s)
+(% c (term s)
+(% f (term (arrow s s))
+
+; -------------------- declaration of input formula -----------------------------------
+
+(% A1 (th_holds (= s a b))
+(% A2 (th_holds (= s b (apply _ _ f c)))
+(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))
+
+
+; ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
+
+(decl_atom (= s a b) (\ v1 (\ a1
+(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
+(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3
+
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(asf _ _ _ a3 (\ l3
+(clausify_false
+
+; this should be a proof of l1 ^ l2 ^ ~l3 => false
+; this is done by theory proof rules (currently just use "trust")
+
+ trust
+
+))))))) (\ CT
+; CT is the clause ( ~v1 V ~v2 V v3 )
+
+; -------------------- clausification of input formulas -----------------------------------------
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A1 is ( ~l1 )
+; the following should be a proof of l1 ^ ( ~l1 ) => false
+; this is done by natural deduction rules
+
+ (contra _ A1 l1)
+
+))) (\ C1
+; C1 is the clause ( v1 )
+
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+; input formula A2 is ( ~l2 )
+; the following should be a proof of l2 ^ ( ~l2 ) => false
+; this is done by natural deduction rules
+
+ (contra _ A2 l2)
+
+))) (\ C2
+; C2 is the clause ( v2 )
+
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(ast _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A3 is ( ~a3 V ~a1 )
+; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
+; this is done by natural deduction rules
+
+ (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))
+
+))))) (\ C3
+; C3 is the clause ( ~v3 V ~v1 )
+
+
+
+; -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ C1
+(R _ _ C2
+(R _ _ CT C3 v3) v2) v1)
+
+(\ x x))
+
+))))))))))))))))))))))))))
+)
\ No newline at end of file diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf new file mode 100755 index 000000000..09255f612 --- /dev/null +++ b/proofs/signatures/sat.plf @@ -0,0 +1,127 @@ +(declare bool type)
+(declare tt bool)
+(declare ff bool)
+
+(declare var type)
+
+(declare lit type)
+(declare pos (! x var lit))
+(declare neg (! x var lit))
+
+(declare clause type)
+(declare cln clause)
+(declare clc (! x lit (! c clause clause)))
+
+; constructs for general clauses for R, Q, satlem
+
+(declare concat (! c1 clause (! c2 clause clause)))
+(declare clr (! l lit (! c clause clause)))
+
+; code to check resolutions
+
+(program append ((c1 clause) (c2 clause)) clause
+ (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
+
+; we use marks as follows:
+; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
+; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
+; -- mark 3 if we did indeed remove the variable positively
+; -- mark 4 if we did indeed remove the variable negatively
+(program simplify_clause ((c clause)) clause
+ (match c
+ (cln cln)
+ ((clc l c1)
+ (match l
+ ; Set mark 1 on v if it is not set, to indicate we should remove it.
+ ; After processing the rest of the clause, set mark 3 if we were already
+ ; supposed to remove v (so if mark 1 was set when we began). Clear mark3
+ ; if we were not supposed to be removing v when we began this call.
+ ((pos v)
+ (let m (ifmarked v tt (do (markvar v) ff))
+ (let c' (simplify_clause c1)
+ (match m
+ (tt (do (ifmarked3 v v (markvar3 v)) c'))
+ (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
+ ; the same as the code for tt, but using different marks.
+ ((neg v)
+ (let m (ifmarked2 v tt (do (markvar2 v) ff))
+ (let c' (simplify_clause c1)
+ (match m
+ (tt (do (ifmarked4 v v (markvar4 v)) c'))
+ (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
+ ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
+ ((clr l c1)
+ (match l
+ ; set mark 1 to indicate we should remove v, and fail if
+ ; mark 3 is not set after processing the rest of the clause
+ ; (we will set mark 3 if we remove a positive occurrence of v).
+ ((pos v)
+ (let m (ifmarked v tt (do (markvar v) ff))
+ (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
+ (let c' (simplify_clause c1)
+ (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
+ (match m (tt v) (ff (markvar v))) c')
+ (fail clause))))))
+ ; same as the tt case, but with different marks.
+ ((neg v)
+ (let m2 (ifmarked2 v tt (do (markvar2 v) ff))
+ (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
+ (let c' (simplify_clause c1)
+ (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
+ (match m2 (tt v) (ff (markvar2 v))) c')
+ (fail clause))))))
+ ))))
+
+
+; resolution proofs
+
+(declare holds (! c clause type))
+
+(declare R (! c1 clause (! c2 clause
+ (! u1 (holds c1)
+ (! u2 (holds c2)
+ (! n var
+ (holds (concat (clr (pos n) c1)
+ (clr (neg n) c2)))))))))
+
+(declare Q (! c1 clause (! c2 clause
+ (! u1 (holds c1)
+ (! u2 (holds c2)
+ (! n var
+ (holds (concat (clr (neg n) c1)
+ (clr (pos n) c2)))))))))
+
+(declare satlem_simplify
+ (! c1 clause
+ (! c2 clause
+ (! c3 clause
+ (! u1 (holds c1)
+ (! r (^ (simplify_clause c1) c2)
+ (! u2 (! x (holds c2) (holds c3))
+ (holds c3))))))))
+
+(declare satlem
+ (! c clause
+ (! c2 clause
+ (! u (holds c)
+ (! u2 (! v (holds c) (holds c2))
+ (holds c2))))))
+
+; A little example to demonstrate simplify_clause.
+; It can handle nested clr's of both polarities,
+; and correctly cleans up marks when it leaves a
+; clr or clc scope. Uncomment and run with
+; --show-runs to see it in action.
+;
+; (check
+; (% v1 var
+; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
+; (clc (pos v1) (clc (pos v1) cln))))
+; (satlem _ _ _ u1 (\ x x))))))
+
+
+;(check
+; (% v1 var
+; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
+; (clr (neg v1) (clc (neg v1) cln)))))
+; (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf new file mode 100755 index 000000000..75bfc442f --- /dev/null +++ b/proofs/signatures/smt.plf @@ -0,0 +1,313 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; SMT syntax and semantics (not theory-specific) +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare formula type) +(declare th_holds (! f formula type)) + +; constants +(declare true formula) +(declare false formula) + +; logical connectives +(declare not (! f formula formula)) +(declare and (! f1 formula (! f2 formula formula))) +(declare or (! f1 formula (! f2 formula formula))) +(declare impl (! f1 formula (! f2 formula formula))) +(declare iff (! f1 formula (! f2 formula formula))) +(declare xor (! f1 formula (! f2 formula formula))) +(declare ifte (! b formula (! f1 formula (! f2 formula formula)))) + +; terms +(declare sort type) ; sort in the theory +(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor + +(declare term (! t sort type)) ; declared terms in formula + +(declare apply (! s1 sort + (! s2 sort + (! t1 (term (arrow s1 s2)) + (! t2 (term s1) + (term s2)))))) + +(declare ite (! s sort + (! f formula + (! t1 (term s) + (! t2 (term s) + (term s)))))) + +; let/flet +(declare let (! s sort + (! t (term s) + (! f (! v (term s) formula) + formula)))) +(declare flet (! f1 formula + (! f2 (! v formula formula) + formula))) + +; predicates +(declare = (! s sort + (! x (term s) + (! y (term s) + formula)))) + +; To avoid duplicating some of the rules (e.g., cong), we will view +; applications of predicates as terms of sort "Bool". +; Such terms can be injected as atomic formulas using "p_app". + +(declare Bool sort) ; the special sort for predicates +(declare p_app (! x (term Bool) formula)) ; propositional application of term + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Examples + +; an example of "(p1 or p2(0)) and t1=t2(1)" +;(! p1 (term Bool) +;(! p2 (term (arrow Int Bool)) +;(! t1 (term Int) +;(! t2 (term (arrow Int Int)) +;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0))) +; (= _ t1 (apply _ _ t2 1)))) +; ... + +; another example of "p3(a,b)" +;(! a (term Int) +;(! b (term Int) +;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc. +;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc. +; ... + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Natural deduction rules : used for CNF +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; contradiction + +(declare contra + (! f formula + (! r1 (th_holds f) + (! r2 (th_holds (not f)) + (th_holds false))))) + +;; not not + +(declare not_not_intro + (! f formula + (! u (th_holds f) + (th_holds (not (not f)))))) + +(declare not_not_elim + (! f formula + (! u (th_holds (not (not f))) + (th_holds f)))) + +;; or elimination + +(declare or_elim_1 + (! f1 formula + (! f2 formula + (! u1 (th_holds (not f1)) + (! u2 (th_holds (or f1 f2)) + (th_holds f2)))))) + +(declare or_elim_2 + (! f1 formula + (! f2 formula + (! u1 (th_holds (not f2)) + (! u2 (th_holds (or f1 f2)) + (th_holds f1)))))) + +;; and elimination + +(declare and_elim_1 + (! f1 formula + (! f2 formula + (! u (th_holds (and f1 f2)) + (th_holds f1))))) + +(declare and_elim_2 + (! f1 formula + (! f2 formula + (! u (th_holds (and f1 f2)) + (th_holds f2))))) + +;; not impl elimination + +(declare not_impl_elim_1 + (! f1 formula + (! f2 formula + (! u (th_holds (not (impl f1 f2))) + (th_holds f1))))) + +(declare not_impl_elim_2 + (! f1 formula + (! f2 formula + (! u (th_holds (not (impl f1 f2))) + (th_holds (not f2)))))) + +;; impl elimination + +(declare impl_intro (! f1 formula + (! f2 formula + (! i1 (! u (th_holds f1) + (th_holds f2)) + (th_holds (impl f1 f2)))))) + +(declare impl_elim + (! f1 formula + (! f2 formula + (! u1 (th_holds f1) + (! u2 (th_holds (impl f1 f2)) + (th_holds f2)))))) + +;; iff elimination + +(declare iff_elim_1 + (! f1 formula + (! f2 formula + (! u1 (th_holds (iff f1 f2)) + (th_holds (impl f1 f2)))))) + +(declare iff_elim_2 + (! f1 formula + (! f2 formula + (! u1 (th_holds (iff f1 f2)) + (th_holds (impl f2 f1)))))) + +(declare not_iff_elim_1 + (! f1 formula + (! f2 formula + (! u1 (th_holds (not f1)) + (! u2 (th_holds (not (iff f1 f2))) + (th_holds f2)))))) + +(declare not_iff_elim_2 + (! f1 formula + (! f2 formula + (! u1 (th_holds f1) + (! u2 (th_holds (not (iff f1 f2))) + (th_holds (not f2))))))) + +;; ite elimination + +(declare ite_elim_1 + (! a formula + (! b formula + (! c formula + (! u1 (th_holds a) + (! u2 (th_holds (ifte a b c)) + (th_holds b))))))) + +(declare ite_elim_2 + (! a formula + (! b formula + (! c formula + (! u1 (th_holds (not a)) + (! u2 (th_holds (ifte a b c)) + (th_holds c))))))) + +(declare ite_elim_3 + (! a formula + (! b formula + (! c formula + (! u1 (th_holds (not b)) + (! u2 (th_holds (ifte a b c)) + (th_holds c))))))) + +(declare ite_elim_2n + (! a formula + (! b formula + (! c formula + (! u1 (th_holds a) + (! u2 (th_holds (ifte (not a) b c)) + (th_holds c))))))) + +(declare not_ite_elim_1 + (! a formula + (! b formula + (! c formula + (! u1 (th_holds a) + (! u2 (th_holds (not (ifte a b c))) + (th_holds (not b)))))))) + +(declare not_ite_elim_2 + (! a formula + (! b formula + (! c formula + (! u1 (th_holds (not a)) + (! u2 (th_holds (not (ifte a b c))) + (th_holds (not c)))))))) + +(declare not_ite_elim_3 + (! a formula + (! b formula + (! c formula + (! u1 (th_holds b) + (! u2 (th_holds (not (ifte a b c))) + (th_holds (not c)))))))) + +(declare not_ite_elim_2n + (! a formula + (! b formula + (! c formula + (! u1 (th_holds a) + (! u2 (th_holds (not (ifte (not a) b c))) + (th_holds (not c)))))))) + + + +;; How to do CNF for disjunctions of theory literals. +;; +;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). +;; +;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn. +;; Do this at the beginning of the proof: +;; +;; (decl_atom F1 (\ v1 (\ a1 +;; (decl_atom F2 (\ v2 (\ a2 +;; .... +;; (decl_atom Fn (\ vn (\ an +;; +;; Our input A is clausified by the following proof: +;; +;;(satlem _ _ +;;(asf _ _ _ a1 (\ l1 +;;(asf _ _ _ a2 (\ l2 +;;... +;;(asf _ _ _ an (\ ln +;;(clausify_false +;; +;; (contra _ +;; (or_elim_1 _ _ l{n-1} +;; ... +;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ l1 A))))) ln) +;; +;;))))))) (\ C +;; +;; We now have the free variable C, which should be the clause (v1 V ... V vn). +;; +;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))). +;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip +;; the arguments of contra: +;; +;;(satlem _ _ +;;(ast _ _ _ a1 (\ l1 +;;(asf _ _ _ a2 (\ l2 +;;(ast _ _ _ a3 (\ l3 +;;(clausify_false +;; +;; (contra _ l3 +;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ (not_not_intro l1) A)))) +;; +;;))))))) (\ C +;; +;; C should be the clause (~v1 V v2 V ~v3 )
\ No newline at end of file diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf new file mode 100755 index 000000000..e66990de4 --- /dev/null +++ b/proofs/signatures/th_base.plf @@ -0,0 +1,107 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Atomization / Clausification
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; binding between an LF var and an (atomic) formula
+(declare atom (! v var (! p formula type)))
+
+(declare decl_atom
+ (! f formula
+ (! u (! v var
+ (! a (atom v f)
+ (holds cln)))
+ (holds cln))))
+
+; direct clausify
+(declare clausify_form
+ (! f formula
+ (! v var
+ (! a (atom v f)
+ (! u (th_holds f)
+ (holds (clc (pos v) cln)))))))
+
+(declare clausify_form_not
+ (! f formula
+ (! v var
+ (! a (atom v f)
+ (! u (th_holds (not f))
+ (holds (clc (neg v) cln)))))))
+
+(declare clausify_false
+ (! u (th_holds false)
+ (holds cln)))
+
+
+(declare th_let_pf
+ (! f formula
+ (! u (th_holds f)
+ (! u2 (! v (th_holds f) (holds cln))
+ (holds cln)))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory reasoning
+; - make a series of assumptions and then derive a contradiction (or false)
+; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
+; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare ast
+ (! v var
+ (! f formula
+ (! C clause
+ (! r (atom v f) ;this is specified
+ (! u (! o (th_holds f)
+ (holds C))
+ (holds (clc (neg v) C))))))))
+
+(declare asf
+ (! v var
+ (! f formula
+ (! C clause
+ (! r (atom v f)
+ (! u (! o (th_holds (not f))
+ (holds C))
+ (holds (clc (pos v) C))))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Equality and Congruence Closure
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; temporary :
+(declare trust (th_holds false))
+
+(declare refl
+ (! s sort
+ (! t (term s)
+ (th_holds (= s t t)))))
+
+(declare symm (! s sort
+ (! x (term s)
+ (! y (term s)
+ (! u (th_holds (= _ x y))
+ (th_holds (= _ y x)))))))
+
+(declare trans (! s sort
+ (! x (term s)
+ (! y (term s)
+ (! z (term s)
+ (! u (th_holds (= _ x y))
+ (! u (th_holds (= _ y z))
+ (th_holds (= _ x z)))))))))
+
+(declare cong (! s1 sort
+ (! s2 sort
+ (! a1 (term (arrow s1 s2))
+ (! b1 (term (arrow s1 s2))
+ (! a2 (term s1)
+ (! b2 (term s1)
+ (! u1 (th_holds (= _ a1 b1))
+ (! u2 (th_holds (= _ a2 b2))
+ (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
+
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c84046570..885a7c487 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -141,7 +141,7 @@ static bool isClosed(Expr e, std::set<Expr>& free, std::hash_set<Expr, ExprHashF if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) { isClosed(e[1], free, closedCache); for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) { - free.erase((*i)[0]); + free.erase(*i); } } else if(e.getKind() == kind::BOUND_VARIABLE) { free.insert(e); @@ -870,10 +870,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - //| /* substring */ - //LPAREN_TOK STRSUB_TOK n1=INTEGER_LITERAL n2=INTEGER_LITERAL RPAREN_TOK - //{ - //} | /* A non-built-in function application */ LPAREN_TOK functionName[name, CHECK_DECLARED] @@ -1250,6 +1246,7 @@ builtinOp[CVC4::Kind& kind] | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } + | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1622,7 +1619,7 @@ INT2BV_TOK : 'int2bv'; //STRCST_TOK : 'str.cst'; STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; -//STRSUB_TOK : 'str.sub' ; +STRSUB_TOK : 'str.sub' ; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; RECON_TOK : 're.++'; diff --git a/src/smt/options b/src/smt/options index 7a72881b4..d2455b520 100644 --- a/src/smt/options +++ b/src/smt/options @@ -49,7 +49,7 @@ option repeatSimp --repeat-simp bool :read-write make multiple passes with nonclausal simplifier option sortInference --sort-inference bool :read-write :default false - apply sort inference to input problem + calculate sort inference of input problem, convert the input based on monotonic sorts common-option incrementalSolving incremental -i --incremental bool enable incremental solving diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 39ccc70c4..be6acd09c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -835,7 +835,7 @@ void SmtEngine::setLogicInternal() throw() { // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { - if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { + if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV) && !d_logic.isTheoryEnabled(THEORY_STRINGS)) { Trace("smt") << "setting theoryof-mode to term-based" << endl; options::theoryOfMode.set(THEORY_OF_TERM_BASED); } @@ -1031,6 +1031,10 @@ void SmtEngine::setLogicInternal() throw() { options::fmfInstGen.set( false ); } } + if ( options::fmfBoundInt() ){ + //if bounded integers are set, must use full model check for MBQI + options::fmfFullModelCheck.set( true ); + } if( options::ufssSymBreak() ){ options::sortInference.set( true ); } @@ -1979,7 +1983,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { } d_nonClausalLearnedLiterals.clear(); - + for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { Node cProp = (*pos).first.eqNode((*pos).second); Assert(d_topLevelSubstitutions.apply(cProp) == cProp); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 186444e0a..0bbef1601 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -32,7 +32,7 @@ class DatatypesRewriter { public: static RewriteResponse postRewrite(TNode in) { - Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl; + Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; if(in.getKind() == kind::APPLY_CONSTRUCTOR ){ Type t = in.getType().toType(); @@ -41,7 +41,7 @@ public: // to ensure a normal form, all parameteric datatype constructors must have a type ascription if( dt.isParametric() ){ if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){ - Trace("datatypes-rewrite") << "Ascribing type to parametric datatype constructor " << in << std::endl; + Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl; Node op = in.getOperator(); //get the constructor object const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())]; @@ -53,7 +53,7 @@ public: children.push_back( op_new ); children.insert( children.end(), in.begin(), in.end() ); Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - Trace("datatypes-rewrite") << "Created " << inr << std::endl; + Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl; return RewriteResponse(REWRITE_DONE, inr); } } @@ -214,7 +214,7 @@ public: } static RewriteResponse preRewrite(TNode in) { - Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl; + Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl; return RewriteResponse(REWRITE_DONE, in); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a0651efb4..c827a8f07 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -26,6 +26,8 @@ #include "smt/options.h" #include "smt/boolean_terms.h" #include "theory/quantifiers/options.h" +#include "theory/datatypes/options.h" +#include "theory/type_enumerator.h" #include <map> @@ -158,15 +160,18 @@ void TheoryDatatypes::check(Effort e) { } } if( !needSplit && mustSpecifyAssignment() ){ + // && //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type //** TODO: this is probably not good enough, actually need fair enumeration strategy + /* Node groundTerm = n.getType().mkGroundTerm(); int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); if( pcons[index] ){ consIndex = index; } needSplit = true; + */ } if( needSplit && consIndex!=-1 ) { Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); @@ -179,7 +184,7 @@ void TheoryDatatypes::check(Effort e) { d_out->requirePhase( test, true ); return; }else{ - Trace("dt-split") << "Do not split constructor for " << n << std::endl; + Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl; } } }else{ @@ -503,6 +508,9 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ trep2 = eqc2->d_constructor.get(); } EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); + + + if( eqc1 ){ if( !eqc1->d_constructor.get().isNull() ){ trep1 = eqc1->d_constructor.get(); @@ -538,6 +546,29 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_inst = true; } if( cons1.isNull() && !cons2.isNull() ){ + Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; + NodeListMap::iterator lbl_i = d_labels.find( t1 ); + if( lbl_i != d_labels.end() ){ + size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr()); + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + if( (*i).getKind()==NOT ){ + if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){ + Node n = *i; + std::vector< TNode > assumptions; + explain( *i, assumptions ); + explain( cons2.eqNode( (*i)[0][0] ), assumptions ); + d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); + Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + } + } + } + checkInst = true; eqc1->d_constructor.set( eqc2->d_constructor ); } @@ -548,14 +579,18 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_inst.set( eqc2->d_inst ); eqc1->d_constructor.set( eqc2->d_constructor ); } + + + //merge labels - Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl; NodeListMap::iterator lbl_i = d_labels.find( t2 ); if( lbl_i != d_labels.end() ){ + Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl; NodeList* lbl = (*lbl_i).second; for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){ addTester( *j, eqc1, t1 ); if( d_conflict ){ + Debug("datatypes-debug") << "Conflict!" << std::endl; return; } } @@ -643,7 +678,7 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ if( !d_conflict ){ - Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl; + Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; bool tpolarity = t.getKind()!=NOT; Node tt = ( t.getKind() == NOT ) ? t[0] : t; int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); @@ -768,6 +803,28 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); m->assertEqualityEngine( &d_equalityEngine ); + + std::vector< TypeEnumerator > vec; + std::map< TypeNode, int > tes; + Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; + + //get all constructors + eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); + std::vector< Node > cons; + while( !eqccs_i.isFinished() ){ + Node eqc = (*eqccs_i); + //for all equivalence classes that are datatypes + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei ){ + if( !ei->d_constructor.get().isNull() ){ + cons.push_back( ei->d_constructor.get() ); + } + } + } + ++eqccs_i; + } + //must choose proper representatives eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ @@ -778,10 +835,63 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( ei ){ if( !ei->d_constructor.get().isNull() ){ //specify that we should use the constructor as the representative - m->assertRepresentative( ei->d_constructor.get() ); + //m->assertRepresentative( ei->d_constructor.get() ); }else{ - Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; + Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; + Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; + + std::vector< bool > pcons; + getPossibleCons( ei, eqc, pcons ); + Trace("dt-cmi") << "Possible constructors : "; + for( unsigned i=0; i<pcons.size(); i++ ){ + Trace("dt-cmi") << pcons[i] << " "; + } + Trace("dt-cmi") << std::endl; + + if( tes.find( eqc.getType() )==tes.end() ){ + tes[eqc.getType()]=vec.size(); + vec.push_back( TypeEnumerator( eqc.getType() ) ); + } + bool success; + Node n; + do { + success = true; + Assert( !vec[tes[eqc.getType()]].isFinished() ); + n = *vec[tes[eqc.getType()]]; + ++vec[tes[eqc.getType()]]; + + //applyTypeAscriptions( n, eqc.getType() ); + + Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl; + //check if it is consistent with labels + size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); + if( constructorIndex<pcons.size() && pcons[constructorIndex] ){ + for( unsigned i=0; i<cons.size(); i++ ){ + //check if it is modulo equality the same + if( cons[i].getOperator()==n.getOperator() ){ + bool diff = false; + for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ + if( !m->areEqual( cons[i][j], n[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; + break; + } + } + } + }else{ + Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl; + success = false; + } + }while( !success ); + Trace("dt-cmi") << "Assign : " << n << std::endl; + //m->assertRepresentative( n ); + m->assertEquality( eqc, n, true ); + } }else{ Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl; @@ -871,7 +981,38 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index return n_ic; //} } - +/* +Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){ + Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + //add type ascription for ambiguous constructor types + if(!n.getType().isComparableTo(tn)) { + size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isParametric() ); + Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl; + Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl; + Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType()); + Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl; + Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() ); + std::vector< Node > children; + children.push_back( op ); + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + children.push_back( applyTypeAscriptions( n[i], TypeNode::fromType( tspec )[i] ) ); + } + n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ) ); + Assert( n.getType()==tn ); + return n; + } + }else{ + if( n.getType()!=tn ){ + Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl; + } + } + return n; +} +*/ void TheoryDatatypes::collapseSelectors(){ //must check incorrect applications of selectors for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){ @@ -918,7 +1059,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ int index = getLabelIndex( eqc, n ); const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); //must be finite or have a selector - if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ + //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ //instantiate this equivalence class eqc->d_inst = true; Node tt_cons = getInstantiateCons( tt, dt, index ); @@ -933,7 +1074,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ d_infer.push_back( eq ); d_infer_exp.push_back( exp ); } - } + //} + //else{ + // Debug("datatypes-inst") << "Do not instantiate" << std::endl; + //} } } @@ -1094,43 +1238,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( DatatypesRewriter::isTermDatatype( eqc ) ){ - Trace( c ) << "DATATYPE : "; - } - Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; - Trace( c ) << " { "; - //add terms to model - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Trace( c ) << (*eqc_i) << " "; - ++eqc_i; - } - Trace( c ) << "}" << std::endl; - if( DatatypesRewriter::isTermDatatype( eqc ) ){ - EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; - if( ei->d_constructor.get().isNull() ){ - Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; - Trace( c ) << " Constructor : " << std::endl; - Trace( c ) << " Labels : "; - if( hasLabel( ei, eqc ) ){ - Trace( c ) << getLabel( eqc ); - }else{ - NodeListMap::iterator lbl_i = d_labels.find( eqc ); - if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ - Trace( c ) << *j << " "; + if( !eqc.getType().isBoolean() ){ + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + Trace( c ) << "DATATYPE : "; + } + Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; + Trace( c ) << " { "; + //add terms to model + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Trace( c ) << (*eqc_i) << " "; + ++eqc_i; + } + Trace( c ) << "}" << std::endl; + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei ){ + Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; + if( ei->d_constructor.get().isNull() ){ + Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; + Trace("debug-model-warn") << " Type : " << eqc.getType() << std::endl; + Trace( c ) << " Constructor : " << std::endl; + Trace( c ) << " Labels : "; + if( hasLabel( ei, eqc ) ){ + Trace( c ) << getLabel( eqc ); + }else{ + NodeListMap::iterator lbl_i = d_labels.find( eqc ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ + Trace( c ) << *j << " "; + } } } + Trace( c ) << std::endl; + }else{ + Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; } - Trace( c ) << std::endl; - }else{ - Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; + Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; } - Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; } } ++eqcs_i; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e38c522c5..203782a79 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -226,6 +226,8 @@ private: void collectTerms( Node n ); /** get instantiate cons */ Node getInstantiateCons( Node n, const Datatype& dt, int index ); + /** apply type ascriptions */ + //Node applyTypeAscriptions( Node n, TypeNode tn ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 778304f32..cec1dccfc 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -37,6 +37,8 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { size_t d_zeroCtor; /** Delegate enumerators for the arguments of the current constructor */ TypeEnumerator** d_argEnumerators; + /** type */ + TypeNode d_type; /** Allocate and initialize the delegate enumerators */ void newEnumerators() { @@ -65,7 +67,8 @@ public: d_datatype(DatatypeType(type.toType()).getDatatype()), d_ctor(0), d_zeroCtor(0), - d_argEnumerators(NULL) { + d_argEnumerators(NULL), + d_type(type) { //Assert(type.isDatatype()); Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl; @@ -76,8 +79,21 @@ public: /* FIXME: this isn't sufficient for mutually-recursive datatypes! */ while(d_zeroCtor < d_datatype.getNumConstructors()) { bool recursive = false; - for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) { - recursive = (Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type); + if( d_datatype.isParametric() ){ + TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) ); + for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){ + if( tn[i]==type ){ + recursive = true; + break; + } + } + }else{ + for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) { + if(Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type) { + recursive = true; + break; + } + } } if(!recursive) { break; @@ -97,7 +113,8 @@ public: d_datatype(de.d_datatype), d_ctor(de.d_ctor), d_zeroCtor(de.d_zeroCtor), - d_argEnumerators(NULL) { + d_argEnumerators(NULL), + d_type(de.d_type) { if(de.d_argEnumerators != NULL) { newEnumerators(); @@ -117,18 +134,33 @@ public: if(d_ctor < d_datatype.getNumConstructors()) { DatatypeConstructor ctor = d_datatype[d_ctor]; NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); - b << ctor.getConstructor(); + Type typ; + if( d_datatype.isParametric() ){ + typ = d_datatype[d_ctor].getSpecializedConstructorType(d_type.toType()); + b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) ); + }else{ + b << ctor.getConstructor(); + } try { for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) { if(d_argEnumerators[a] == NULL) { - d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]); + if( d_datatype.isParametric() ){ + d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType( typ )[a]); + }else{ + d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]); + } } b << **d_argEnumerators[a]; } } catch(NoMoreValuesException&) { InternalError(); } - return Node(b); + Node nnn = Node(b); + //if( nnn.getType()!=d_type || !nnn.getType().isComparableTo(d_type) ){ + // Debug("dt-warn") << "WARNING : Enum : " << nnn << " bad type : " << nnn.getType() << " " << d_type << std::endl; + //} + return nnn; } else { throw NoMoreValuesException(getType()); } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index cb8cb8154..b1a0c4ed4 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -139,6 +139,11 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); + + //flatten the representatives + //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; + //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); + //for debugging if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); @@ -149,7 +154,7 @@ int ModelEngine::checkModel(){ Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); for( size_t i=0; i<it->second.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; - Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 57211ade7..fd114df04 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -98,7 +98,7 @@ option finiteModelFind --finite-model-find bool :default false option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding -option fmfFullModelCheck --fmf-fmc bool :default false +option fmfFullModelCheck --fmf-fmc bool :default false :read-write enable full model check for finite model finding option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0fe50aad6..c14ee01ce 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -102,7 +102,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_eq_query; } -EqualityQuery* QuantifiersEngine::getEqualityQuery() { +EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } @@ -594,8 +594,9 @@ Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ eq::EqualityEngine* ee = getEngine(); if( ee->hasTerm( a ) ){ return ee->getRepresentative( a ); + }else{ + return a; } - return a; } bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ @@ -631,66 +632,126 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( !options::internalReps() ){ return r; }else{ - int sortId = 0; - if( optInternalRepSortInference() ){ - //if( options::ufssSymBreak() ){ - sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] ); - } - if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){ + if( d_int_rep.find( r )==d_int_rep.end() ){ //find best selection for representative Node r_best; - if( options::fmfRelevantDomain() ){ + if( options::fmfRelevantDomain() && !f.isNull() ){ Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r ); Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; }else{ std::vector< Node > eqc; getEquivalenceClass( r, eqc ); + Trace("internal-rep-select") << "Choose representative for equivalence class : { "; + for( unsigned i=0; i<eqc.size(); i++ ){ + if( i>0 ) Trace("internal-rep-select") << ", "; + Trace("internal-rep-select") << eqc[i]; + } + Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index ); + //if cbqi is active, do not choose instantiation constant terms if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){ - if( optInternalRepSortInference() ){ - int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]); - if( score>=0 && e_sortId!=sortId ){ - score += 100; - } - } + int score = getRepScore( eqc[i], f, index ); //score prefers earliest use of this term as a representative if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ r_best = eqc[i]; r_best_score = score; } - } + } } if( r_best.isNull() ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - } + if( !f.isNull() ){ + Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); + r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + }else{ + r_best = a; + } + } //now, make sure that no other member of the class is an instance - if( !optInternalRepSortInference() ){ - r_best = getInstance( r_best, eqc ); - } + r_best = getInstance( r_best, eqc ); //store that this representative was chosen at this point if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } + Trace("internal-rep-select") << "...Choose " << r_best << std::endl; } - d_int_rep[sortId][r] = r_best; + d_int_rep[r] = r_best; if( r_best!=a ){ Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; } - if( optInternalRepSortInference() ){ - int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best ); - if( sortId!=sortIdBest ){ - Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl; - } - } return r_best; }else{ - return d_int_rep[sortId][r]; + return d_int_rep[r]; + } + } +} + +void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) { + //make sure internal representatives currently exist + for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){ + if( it->first.isSort() ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + Node r = getInternalRepresentative( it->second[i], Node::null(), 0 ); + } + } + } + Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; + for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ + Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + } + //store representatives for newly created terms + std::map< Node, Node > temp_rep_map; + + bool success; + do { + success = false; + for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ + if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ + Node ni = it->second; + std::vector< Node > cc; + cc.push_back( it->second.getOperator() ); + bool changed = false; + for( unsigned j=0; j<ni.getNumChildren(); j++ ){ + if( ni[j].getType().isSort() ){ + Node r = getRepresentative( ni[j] ); + if( d_int_rep.find( r )==d_int_rep.end() ){ + Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); + r = temp_rep_map[r]; + } + if( r==ni ){ + //found sub-term as instance + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; + d_int_rep[it->first] = ni[j]; + changed = false; + success = true; + break; + }else{ + Node ir = d_int_rep[r]; + cc.push_back( ir ); + if( ni[j]!=ir ){ + changed = true; + } + } + }else{ + changed = false; + break; + } + } + if( changed ){ + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; + success = true; + d_int_rep[it->first] = n; + temp_rep_map[n] = it->first; + } + } } + }while( success ); + Trace("internal-rep-flatten") << "---After flattening : " << std::endl; + for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ + Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; } } @@ -750,6 +811,3 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } -bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() { - return false; //shown to be not effective -} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index b075f7be8..8f645afe7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -142,7 +142,7 @@ public: TheoryEngine* getTheoryEngine() { return d_te; } /** get equality query object for the given type. The default is the generic one */ - EqualityQuery* getEqualityQuery(); + EqualityQueryQuantifiersEngine* getEqualityQuery(); /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } /** get model engine */ @@ -277,7 +277,7 @@ private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** internal representatives */ - std::map< int, std::map< Node, Node > > d_int_rep; + std::map< Node, Node > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; /** reset count */ @@ -289,8 +289,6 @@ private: Node getInstance( Node n, std::vector< Node >& eqc ); /** get score */ int getRepScore( Node n, Node f, int index ); - /** choose rep based on sort inference */ - bool optInternalRepSortInference(); public: EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){} ~EqualityQueryQuantifiersEngine(){} @@ -308,6 +306,8 @@ public: not contain instantiation constants, if such a term exists. */ Node getInternalRepresentative( Node a, Node f, int index ); + /** flatten representatives */ + void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); void setLiberal( bool l ) { d_liberal = l; } }; /* EqualityQueryQuantifiersEngine */ diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 814276a7c..fe7b9b3d9 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -16,6 +16,8 @@ operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" +operator STRING_SUBSTR 3 "string substr" + #sort CHAR_TYPE \ # Cardinality::INTEGERS \ # well-founded \ @@ -99,6 +101,7 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule +typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7d5edd0f7..a0058954d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -96,14 +96,18 @@ bool TheoryStrings::areDisequal( Node a, Node b ){ } } -Node TheoryStrings::getLength( Node t ) { - EqcInfo * ei = getOrMakeEqcInfo( t ); - Node length_term = ei->d_length_term; +Node TheoryStrings::getLengthTerm( Node t ) { + EqcInfo * ei = getOrMakeEqcInfo( t, false ); + Node length_term = ei ? ei->d_length_term : Node::null(); if( length_term.isNull()) { //typically shouldnt be necessary length_term = t; } - return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ); + return length_term; +} + +Node TheoryStrings::getLength( Node t ) { + return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ); } void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -194,23 +198,29 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { seperateByLength( nodes, col, lts ); //step 1 : get all values for known lengths std::vector< Node > lts_values; - //std::map< Node, bool > values_used; + std::map< unsigned, bool > values_used; for( unsigned i=0; i<col.size(); i++ ){ - Trace("strings-model") << "Checking length for " << col[i][0] << " (length is " << lts[i] << ")" << std::endl; + Trace("strings-model") << "Checking length for {"; + for( unsigned j=0; j<col[i].size(); j++ ){ + if( j>0 ) Trace("strings-model") << ", "; + Trace("strings-model") << col[i][j]; + } + Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl; if( lts[i].isConst() ){ lts_values.push_back( lts[i] ); - //values_used[ lts[i] ] = true; + unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt(); + values_used[ lvalue ] = true; }else{ //get value for lts[i]; if( !lts[i].isNull() ){ Node v = d_valuation.getModelValue(lts[i]); - //Node v = m->getValue(lts[i]); Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; lts_values.push_back( v ); - //values_used[ v ] = true; + unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt(); + values_used[ lvalue ] = true; }else{ - Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; - Assert( false ); + //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; + //Assert( false ); lts_values.push_back( Node::null() ); } } @@ -240,26 +250,39 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { } Trace("strings-model") << "have length " << lts_values[i] << std::endl; - Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; - for( unsigned j=0; j<pure_eq.size(); j++ ){ - Trace("strings-model") << pure_eq[j] << " "; - } - Trace("strings-model") << std::endl; - - //use type enumerator - StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); - for( unsigned j=0; j<pure_eq.size(); j++ ){ - Assert( !sel.isFinished() ); - Node c = *sel; - while( d_equalityEngine.hasTerm( c ) ){ - ++sel; + //assign a new length if necessary + if( !pure_eq.empty() ){ + if( lts_values[i].isNull() ){ + unsigned lvalue = 0; + while( values_used.find( lvalue )!=values_used.end() ){ + lvalue++; + } + Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl; + lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) ); + values_used[ lvalue ] = true; + } + Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; + for( unsigned j=0; j<pure_eq.size(); j++ ){ + Trace("strings-model") << pure_eq[j] << " "; + } + Trace("strings-model") << std::endl; + + + //use type enumerator + StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); + for( unsigned j=0; j<pure_eq.size(); j++ ){ Assert( !sel.isFinished() ); - c = *sel; + Node c = *sel; + while( d_equalityEngine.hasTerm( c ) ){ + ++sel; + Assert( !sel.isFinished() ); + c = *sel; + } + ++sel; + Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl; + processed[pure_eq[j]] = c; + m->assertEquality( pure_eq[j], c, true ); } - ++sel; - Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl; - processed[pure_eq[j]] = c; - m->assertEquality( pure_eq[j], c, true ); } } Trace("strings-model") << "String Model : Finished." << std::endl; @@ -363,74 +386,30 @@ void TheoryStrings::check(Effort e) { bool addedLemma = false; if( e == EFFORT_FULL && !d_conflict ) { - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - //if eqc.getType is string - if (eqc.getType().isString()) { - //EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); - //get the constant for the equivalence class - //int c_len = ...; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = (*eqc_i); - - //if n is concat, and - //if n has not instantiatied the concat..length axiom - //then, add lemma - if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){ - if( d_length_inst.find(n)==d_length_inst.end() ){ - d_length_inst[n] = true; - Trace("strings-debug") << "get n: " << n << endl; - Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); - d_length_intro_vars.push_back( sk ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); - eq = Rewriter::rewrite(eq); - Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl; - d_out->lemma(eq); - Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node lsum; - if( n.getKind() == kind::STRING_CONCAT ){ - //add lemma - std::vector<Node> node_vec; - for( unsigned i=0; i<n.getNumChildren(); i++ ) { - Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] ); - node_vec.push_back(lni); - } - lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); - }else{ - //add lemma - lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) ); - } - Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); - ceq = Rewriter::rewrite(ceq); - Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl; - d_out->lemma(ceq); - addedLemma = true; - } - } - ++eqc_i; - } - } - ++eqcs_i; - } - if( !addedLemma ){ - addedLemma = checkNormalForms(); - Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if(!d_conflict && !addedLemma) { - addedLemma = checkCardinality(); - Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if( !d_conflict && !addedLemma ){ - addedLemma = checkInductiveEquations(); - Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - } - } - } + addedLemma = checkLengths(); + Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if( !addedLemma ){ + addedLemma = checkNormalForms(); + Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if(!d_conflict && !addedLemma) { + addedLemma = checkLengthsEqc(); + Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if(!d_conflict && !addedLemma) { + addedLemma = checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if( !d_conflict && !addedLemma ){ + addedLemma = checkInductiveEquations(); + Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + } + } + } + } } + Trace("strings-check") << "Theory of strings, done check : " << e << std::endl; Trace("strings-process") << "Theory of strings, done check : " << e << std::endl; } -TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) { +TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { } @@ -492,6 +471,9 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); } + if( !e2->d_normalized_length.get().isNull() ){ + e1->d_normalized_length.set( e2->d_normalized_length ); + } } if( hasTerm( d_zero ) ){ Node leqc; @@ -572,16 +554,17 @@ void TheoryStrings::doPendingLemmas() { } } -void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, +bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) { // EqcItr eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ) { Node n = (*eqc_i); - Trace("strings-process") << "Process term " << n << std::endl; + Trace("strings-process-debug") << "Get Normal Form : Process term " << n << std::endl; if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { std::vector<Node> nf_n; std::vector<Node> nf_exp_n; + bool result = true; if( n.getKind() == kind::CONST_STRING ){ if( n!=d_emptyString ) { nf_n.push_back( n ); @@ -591,37 +574,88 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std Node nr = d_equalityEngine.getRepresentative( n[i] ); std::vector< Node > nf_temp; std::vector< Node > nf_exp_temp; - Trace("strings-process") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; - normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + bool nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return; - } - if( nf.size()!=1 || nf[0]!=d_emptyString ) { - for( unsigned r=0; r<nf_temp.size(); r++ ) { - Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT ); - } - nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() ); - } - nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() ); - if( nr!=n[i] ) { - nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); + return true; } + //successfully computed normal form + if( nf.size()!=1 || nf[0]!=d_emptyString ) { + for( unsigned r=0; r<nf_temp.size(); r++ ) { + Assert( !nresult || nf_temp[r].getKind()!=kind::STRING_CONCAT ); + } + nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() ); + } + nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() ); + if( nr!=n[i] ) { + nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); + } + if( !nresult ){ + //Trace("strings-process-debug") << "....Caused already asserted + for( unsigned j=i+1; j<n.getNumChildren(); j++ ){ + if( !areEqual( n[j], d_emptyString ) ){ + nf_n.push_back( n[j] ); + } + } + if( nf_n.size()>1 ){ + result = false; + break; + } + } } } - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); + if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){ + if( nf_n.size()>1 ){ + Trace("strings-process-debug") << "Check for component lemmas for normal form "; + printConcat(nf_n,"strings-process-debug"); + Trace("strings-process-debug") << "..." << std::endl; + for( unsigned i=0; i<nf_n.size(); i++ ){ + //if a component is equal to whole, + if( areEqual( nf_n[i], n ) ){ + //all others must be empty + std::vector< Node > ant; + if( nf_n[i]!=n ){ + ant.push_back( nf_n[i].eqNode( n ) ); + } + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + std::vector< Node > cc; + for( unsigned j=0; j<nf_n.size(); j++ ){ + if( i!=j ){ + cc.push_back( nf_n[j].eqNode( d_emptyString ) ); + } + } + std::vector< Node > empty_vec; + Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); + sendLemma( mkExplain( ant ), conc, "Component" ); + return true; + } + } + } + if( !result ){ + //we have a normal form that will cause a component lemma at a higher level + normal_forms.clear(); + normal_forms_exp.clear(); + normal_form_src.clear(); + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + if( !result ){ + return false; + } + }else{ + Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; + //Assert( areEqual( nf_n[0], eqc ) ); + if( !areEqual( nn, eqc ) ){ + std::vector< Node > ant; + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + ant.push_back( n.eqNode( eqc ) ); + Node conc = nn.eqNode( eqc ); + sendLemma( mkExplain( ant ), conc, "Trivial Equal Normal Form" ); + return true; + } + } } - /* should we add these? - else { - //var/sk? - std::vector<Node> nf_n; - std::vector<Node> nf_exp_n; - nf_n.push_back(n); - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); - }*/ ++eqc_i; } @@ -647,29 +681,36 @@ void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std Trace("strings-solve") << std::endl; } } + return true; } //nf_exp is conjunction -void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { +bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { Trace("strings-process") << "Process equivalence class " << eqc << std::endl; if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){ - //nf.push_back( eqc ); + nf.push_back( eqc ); + /* if( eqc.getKind()==kind::STRING_CONCAT ){ for( unsigned i=0; i<eqc.getNumChildren(); i++ ){ - if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){ + if( !areEqual( eqc[i], d_emptyString ) ){ nf.push_back( eqc[i] ); } } - }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){ + }else if( !areEqual( eqc, d_emptyString ) ){ nf.push_back( eqc ); } + */ Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; - } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){ + return false; + } else if( areEqual( eqc, d_emptyString ) ){ //do nothing Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl; + d_normal_forms_base[eqc] = d_emptyString; d_normal_forms[eqc].clear(); d_normal_forms_exp[eqc].clear(); + return true; } else { visited.push_back( eqc ); + bool result; if(d_normal_forms.find(eqc)==d_normal_forms.end() ){ //phi => t = s1 * ... * sn // normal form for each non-variable term in this eqc (s1...sn) @@ -679,302 +720,336 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v // record terms for each normal form (t) std::vector< Node > normal_form_src; //Get Normal Forms - getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); + result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return; - } - - unsigned i = 0; - //unify each normal form > 0 with normal_forms[0] - for( unsigned j=1; j<normal_forms.size(); j++ ) { - - Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl; - if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){ - Trace("strings-solve") << "Already normalized (in cache)." << std::endl; - }else{ - Trace("strings-solve") << "Not in cache." << std::endl; - //the current explanation for why the prefix is equal - std::vector< Node > curr_exp; - curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); - curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); - curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); - //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality - unsigned index_i = 0; - unsigned index_j = 0; - bool success; - do - { - success = false; - //if we are at the end - if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { - if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){ - //we're done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - }else{ - //the remainder must be empty - unsigned k = index_i==normal_forms[i].size() ? j : i; - unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; - while(!d_conflict && index_k<normal_forms[k].size()) { - //can infer that this string must be empty - Node eq_exp; - if( curr_exp.empty() ) { - eq_exp = d_true; - } else if( curr_exp.size() == 1 ) { - eq_exp = curr_exp[0]; - } else { - eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp ); - } - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); - Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) ); - d_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - index_k++; - } - } - }else { - Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl; - if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){ - Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl; - //terms are equal, continue - if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){ - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i], - normal_forms[j][index_j]); - Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; - curr_exp.push_back(eq); - } - index_j++; - index_i++; - success = true; - }else{ - Node length_term_i = getLength( normal_forms[i][index_i] ); - Node length_term_j = getLength( normal_forms[j][index_j] ); - //check if length(normal_forms[i][index]) == length(normal_forms[j][index]) - if( areEqual(length_term_i, length_term_j) ){ - Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl; - //length terms are equal, merge equivalence classes if not already done so - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); - std::vector< Node > temp_exp; - temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); - temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j )); - Node eq_exp = temp_exp.empty() ? d_true : - temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); - Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - //d_equalityEngine.assertEquality( eq, true, eq_exp ); - d_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - return; - }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || - ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){ - Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; - Node conc; - std::vector< Node > antec; - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - std::vector< Node > antec_new_lits; - std::vector< Node > eqn; - for( unsigned r=0; r<2; r++ ){ - int index_k = r==0 ? index_i : index_j; - int k = r==0 ? i : j; - std::vector< Node > eqnc; - for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){ - eqnc.push_back( normal_forms[k][index_l] ); + return true; + }else if( result ){ + unsigned i = 0; + //unify each normal form > 0 with normal_forms[0] + for( unsigned j=1; j<normal_forms.size(); j++ ) { + Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl; + if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){ + Trace("strings-solve") << "Already normalized (in cache)." << std::endl; + }else{ + Trace("strings-solve") << "Not in cache." << std::endl; + //the current explanation for why the prefix is equal + std::vector< Node > curr_exp; + curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); + curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); + curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); + //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality + unsigned index_i = 0; + unsigned index_j = 0; + bool success; + do + { + success = false; + //if we are at the end + if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { + if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){ + //we're done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + }else{ + //the remainder must be empty + unsigned k = index_i==normal_forms[i].size() ? j : i; + unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; + while(!d_conflict && index_k<normal_forms[k].size()) { + //can infer that this string must be empty + Node eq_exp; + if( curr_exp.empty() ) { + eq_exp = d_true; + } else if( curr_exp.size() == 1 ) { + eq_exp = curr_exp[0]; + } else { + eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp ); } - eqn.push_back( mkConcat( eqnc ) ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); + Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + index_k++; + } + } + }else { + Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl; + if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){ + Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl; + //terms are equal, continue + if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){ + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i], + normal_forms[j][index_j]); + Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; + curr_exp.push_back(eq); } - conc = eqn[0].eqNode( eqn[1] ); - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Endpoint" ); - return; + index_j++; + index_i++; + success = true; }else{ - Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl; - Node conc; - std::vector< Node > antec; - std::vector< Node > antec_new_lits; - //check for loops - //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; - int has_loop[2] = { -1, -1 }; - for( unsigned r=0; r<2; r++ ){ - int index = (r==0 ? index_i : index_j); - int other_index = (r==0 ? index_j : index_i ); - int n_index = (r==0 ? i : j); - int other_n_index = (r==0 ? j : i); - if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { - for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){ - if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){ - has_loop[r] = lp; - break; - } - } - } - } - if( has_loop[0]!=-1 || has_loop[1]!=-1 ){ - int loop_n_index = has_loop[0]!=-1 ? i : j; - int other_n_index = has_loop[0]!=-1 ? j : i; - int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1]; - int index = has_loop[0]!=-1 ? index_i : index_j; - int other_index = has_loop[0]!=-1 ? index_j : index_i; - Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index]; - Trace("strings-loop") << " ... " << normal_forms[other_n_index][other_index] << std::endl; - - //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp - //check if - //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z - // and - //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y - // for some y,z,k - - Trace("strings-loop") << "Must add lemma." << std::endl; - //need to break - Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - + Node length_term_i = getLength( normal_forms[i][index_i] ); + Node length_term_j = getLength( normal_forms[j][index_j] ); + //check length(normal_forms[i][index]) == length(normal_forms[j][index]) + if( !areDisequal(length_term_i, length_term_j) && + normal_forms[i][index_i].getKind()!=kind::CONST_STRING && + normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) { + + //length terms are equal, merge equivalence classes if not already done so + Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); + if( !areEqual(length_term_i, length_term_j) ) { + Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; + //try to make the lengths equal via splitting on demand + sendSplit( length_term_i, length_term_j, "Length" ); + length_eq = Rewriter::rewrite( length_eq ); + d_pending_req_phase[ length_eq ] = true; + return true; + }else{ + Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl; + //lengths are already equal, do unification + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); + std::vector< Node > temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(length_eq); + Node eq_exp = temp_exp.empty() ? d_true : + temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); + Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + return true; + } + }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || + ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){ + Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; + Node conc; + std::vector< Node > antec; antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - //require that x is non-empty - Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ); - x_empty = Rewriter::rewrite( x_empty ); - //if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){ - // antec.push_back( x_empty.negate() ); - //}else{ - antec_new_lits.push_back( x_empty.negate() ); - //} - d_pending_req_phase[ x_empty ] = true; - - - //t1 * ... * tn = y * z - std::vector< Node > c1c; - //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] - for( int r=index; r<=loop_index-1; r++ ) { - c1c.push_back( normal_forms[loop_n_index][r] ); + std::vector< Node > antec_new_lits; + std::vector< Node > eqn; + for( unsigned r=0; r<2; r++ ){ + int index_k = r==0 ? index_i : index_j; + int k = r==0 ? i : j; + std::vector< Node > eqnc; + for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){ + eqnc.push_back( normal_forms[k][index_l] ); + } + eqn.push_back( mkConcat( eqnc ) ); } - Node conc1 = mkConcat( c1c ); - conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); - std::vector< Node > c2c; - //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] - for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { - c2c.push_back( normal_forms[other_n_index][r] ); + if( areEqual( eqn[0], eqn[1] ) ){ + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + }else{ + conc = eqn[0].eqNode( eqn[1] ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Endpoint" ); + return true; } - Node left2 = mkConcat( c2c ); - std::vector< Node > c3c; - c3c.push_back( sk_z ); - c3c.push_back( sk_y ); - //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] - for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { - c3c.push_back( normal_forms[loop_n_index][r] ); + }else{ + Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl; + Node conc; + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + //check for loops + //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; + int has_loop[2] = { -1, -1 }; + for( unsigned r=0; r<2; r++ ){ + int index = (r==0 ? index_i : index_j); + int other_index = (r==0 ? index_j : index_i ); + int n_index = (r==0 ? i : j); + int other_n_index = (r==0 ? j : i); + if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { + for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){ + if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){ + has_loop[r] = lp; + break; + } + } + } } - Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, - mkConcat( c3c ) ); - - Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); - //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); - //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero); - //Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero); - //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString); - //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero); - - //Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate(); - //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, - // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), - // sk_y_len ); - Node ant = mkExplain( antec, antec_new_lits ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y - - //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); - //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); - - //we will be done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - sendLemma( ant, conc, "Loop" ); - addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" ); - return; - }else{ - Trace("strings-solve-debug") << "No loops detected." << std::endl; - if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || - normal_forms[j][index_j].getKind() == kind::CONST_STRING) { - unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; - unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; - unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; - unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; - Node const_str = normal_forms[const_k][const_index_k]; - Node other_str = normal_forms[nconst_k][nconst_index_k]; - if( other_str.getKind() == kind::CONST_STRING ) { - unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size(); - if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) { - //same prefix - //k is the index of the string that is shorter - int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j; - int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j; - int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i; - int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i; - Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) ); - Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; - normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); - normal_forms[l][index_l] = normal_forms[k][index_k]; - success = true; - } else { - //curr_exp is conflict - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + if( has_loop[0]!=-1 || has_loop[1]!=-1 ){ + int loop_n_index = has_loop[0]!=-1 ? i : j; + int other_n_index = has_loop[0]!=-1 ? j : i; + int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1]; + int index = has_loop[0]!=-1 ? index_i : index_j; + int other_index = has_loop[0]!=-1 ? index_j : index_i; + Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index]; + Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl; + + Trace("strings-loop") << " ... T(Y.Z)= "; + for(int lp=index; lp<loop_index; ++lp) { + if(lp != index) Trace("strings-loop") << " ++ "; + Trace("strings-loop") << normal_forms[loop_n_index][lp]; + } + Trace("strings-loop") << std::endl; + Trace("strings-loop") << " ... S(Z.Y)= "; + for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) { + if(lp != other_index+1) Trace("strings-loop") << " ++ "; + Trace("strings-loop") << normal_forms[other_n_index][lp]; + } + Trace("strings-loop") << std::endl; + Trace("strings-loop") << " ... R= "; + for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) { + if(lp != loop_index+1) Trace("strings-loop") << " ++ "; + Trace("strings-loop") << normal_forms[loop_n_index][lp]; + } + Trace("strings-loop") << std::endl; + + //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp + //check if + //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z + // and + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y + // for some y,z,k + + Trace("strings-loop") << "Must add lemma." << std::endl; + //need to break + Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + //require that x is non-empty + Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ); + x_empty = Rewriter::rewrite( x_empty ); + //if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){ + // antec.push_back( x_empty.negate() ); + //}else{ + antec_new_lits.push_back( x_empty.negate() ); + //} + d_pending_req_phase[ x_empty ] = true; + + + //t1 * ... * tn = y * z + std::vector< Node > c1c; + //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] + for( int r=index; r<=loop_index-1; r++ ) { + c1c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc1 = mkConcat( c1c ); + conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + std::vector< Node > c2c; + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] + for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { + c2c.push_back( normal_forms[other_n_index][r] ); + } + Node left2 = mkConcat( c2c ); + std::vector< Node > c3c; + c3c.push_back( sk_z ); + c3c.push_back( sk_y ); + //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] + for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { + c3c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, + mkConcat( c3c ) ); + + Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); + //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero); + //Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero); + //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString); + //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero); + + //Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate(); + //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), + // sk_y_len ); + Node ant = mkExplain( antec, antec_new_lits ); + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y + + //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); + //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); + + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + sendLemma( ant, conc, "Loop" ); + addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" ); + return true; + }else{ + Trace("strings-solve-debug") << "No loops detected." << std::endl; + if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || + normal_forms[j][index_j].getKind() == kind::CONST_STRING) { + unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; + unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; + unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; + unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; + Node const_str = normal_forms[const_k][const_index_k]; + Node other_str = normal_forms[nconst_k][nconst_index_k]; + if( other_str.getKind() == kind::CONST_STRING ) { + unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size(); + if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) { + //same prefix + //k is the index of the string that is shorter + int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j; + int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j; + int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i; + int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i; + Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; + normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); + normal_forms[l][index_l] = normal_forms[k][index_k]; + success = true; + } else { + //curr_exp is conflict + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return true; + } + } else { + Assert( other_str.getKind()!=kind::STRING_CONCAT ); + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); + //split the string + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); + + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); + Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Conflict" ); - return; - } - } else { - Assert( other_str.getKind()!=kind::STRING_CONCAT ); - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); - //split the string - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); - - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); - Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); - Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero ); + sendLemma( ant, conc, "Constant Split" ); + return true; + } + }else{ + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + antec.push_back( ldeq ); + }else{ + antec_new_lits.push_back(ldeq); + } + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); + Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + // |sk| > 0 + //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); + Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); + Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + //d_out->lemma(sk_gt_zero); + d_lemma_cache.push_back( sk_gt_zero ); Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Constant Split" ); - return; - } - }else{ - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - - Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); - if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ - antec.push_back( ldeq ); - }else{ - antec_new_lits.push_back(ldeq); + sendLemma( ant, conc, "Split" ); + return true; } - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); - Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - // |sk| > 0 - //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); - Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); - Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; - //d_out->lemma(sk_gt_zero); - d_lemma_cache.push_back( sk_gt_zero ); - - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Split" ); - return; - } - } - } - } - } - }while(success); - } - } + } + } + } + } + }while(success); + } + } + } //construct the normal form if( normal_forms.empty() ){ @@ -990,73 +1065,150 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl; } - //if( visited.empty() ){ - //TODO : cache? - //} + + d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0]; d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() ); d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() ); - Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl; + Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl; }else{ - Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl; + Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl; nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() ); nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() ); + result = true; } visited.pop_back(); + return result; } } bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { //Assert( areDisequal( ni, nj ) ); if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){ + std::vector< Node > nfi; + nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); + std::vector< Node > nfj; + nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); + unsigned index = 0; - while( index<d_normal_forms[ni].size() ){ - Node i = d_normal_forms[ni][index]; - Node j = d_normal_forms[nj][index]; - Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; - if( !areEqual( i, j ) ){ - Node li = getLength( i ); - Node lj = getLength( j ); - if( !areEqual(li, lj) ){ - Trace("strings-solve") << "Case 2 : add lemma " << std::endl; - //must add lemma - std::vector< Node > antec; - std::vector< Node > antec_new_lits; - antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); - antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); - antec.push_back( ni.eqNode( nj ).negate() ); - antec_new_lits.push_back( li.eqNode( lj ) ); - std::vector< Node > conc; - Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" ); - Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" ); - Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" ); - Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ); - Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 ); - Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 ); - conc.push_back( s_eq_w1w2w3 ); - Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 ); - conc.push_back( t_eq_w1w4w5 ); - Node w2_neq_w4 = sk2.eqNode( sk4 ).negate(); - conc.push_back( w2_neq_w4 ); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); - Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one); - conc.push_back( w2_len_one ); - Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one); - conc.push_back( w4_len_one ); - - //Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), - // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) ); - //conc.push_back( eq ); - sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" ); - return true; - }else if( areDisequal( i, j ) ){ - Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl; - //we are done - return false; + while( index<nfi.size() || index<nfj.size() ){ + if( index>=nfi.size() || index>=nfj.size() ){ + std::vector< Node > ant; + //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict + Node lni = getLength( ni ); + Node lnj = getLength( nj ); + ant.push_back( lni.eqNode( lnj ) ); + ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) ); + ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) ); + ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); + ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + std::vector< Node > cc; + std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi; + for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){ + cc.push_back( nfk[index_k].eqNode( d_emptyString ) ); + } + Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); + conc = Rewriter::rewrite( conc ); + sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty"); + return true; + }else{ + Node i = nfi[index]; + Node j = nfj[index]; + Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + if( !areEqual( i, j ) ) { + if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ){ + unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size(); + String si = i.getConst<String>().substr(0, len_short); + String sj = j.getConst<String>().substr(0, len_short); + if(si == sj) { + if( i.getConst<String>().size() < j.getConst<String>().size() ) { + Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << nfj[index] << " into " << nfi[index] << ", " << remainderStr << std::endl; + nfj.insert( nfj.begin() + index + 1, remainderStr ); + nfj[index] = nfi[index]; + } else { + Node remainderStr = NodeManager::currentNM()->mkConst( i.getConst<String>().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << nfi[index] << " into " << nfj[index] << ", " << remainderStr << std::endl; + nfi.insert( nfi.begin() + index + 1, remainderStr ); + nfi[index] = nfj[index]; + } + } else { + //conflict + return false; + } + }else{ + Node li = getLength( i ); + Node lj = getLength( j ); + if( areDisequal(li, lj) ){ + Trace("strings-solve") << "Case 2 : add lemma " << std::endl; + //must add lemma + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); + antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + antec.push_back( ni.eqNode( nj ).negate() ); + antec_new_lits.push_back( li.eqNode( lj ).negate() ); + std::vector< Node > conc; + Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" ); + Node lsk1 = getLength( sk1 ); + conc.push_back( lsk1.eqNode( li ) ); + Node lsk2 = getLength( sk2 ); + conc.push_back( lsk2.eqNode( lj ) ); + conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, + j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); + + /* + Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" ); + Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ); + Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 ); + Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 ); + conc.push_back( s_eq_w1w2w3 ); + Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 ); + conc.push_back( t_eq_w1w4w5 ); + Node w2_neq_w4 = sk2.eqNode( sk4 ).negate(); + conc.push_back( w2_neq_w4 ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); + Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one); + conc.push_back( w2_len_one ); + Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one); + conc.push_back( w4_len_one ); + Node c = NodeManager::currentNM()->mkNode( kind::AND, conc ); + */ + //Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) ); + //conc.push_back( eq ); + sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" ); + return true; + }else if( areEqual( li, lj ) ){ + if( areDisequal( i, j ) ){ + Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl; + //we are done + return false; + } else { + //splitting on demand : try to make them disequal + Node eq = i.eqNode( j ); + sendSplit( i, j, "Disequality : disequal terms" ); + eq = Rewriter::rewrite( eq ); + d_pending_req_phase[ eq ] = false; + return true; + } + }else{ + //splitting on demand : try to make lengths equal + Node eq = li.eqNode( lj ); + sendSplit( li, lj, "Disequality : equal length" ); + eq = Rewriter::rewrite( eq ); + d_pending_req_phase[ eq ] = true; + return true; + } + } } + index++; } - index++; } Assert( false ); } @@ -1183,7 +1335,7 @@ bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, cons } void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { - if( conc.isNull() ){ + if( conc.isNull() || conc==d_false ){ d_out->conflict(ant); Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl; d_conflict = true; @@ -1204,11 +1356,23 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c ) { d_pending_req_phase[eq] = true; } +Node TheoryStrings::mkConcat( Node n1, Node n2 ) { + std::vector< Node > c; + c.push_back( n1 ); + c.push_back( n2 ); + return mkConcat( c ); +} + Node TheoryStrings::mkConcat( std::vector< Node >& c ) { Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); return Rewriter::rewrite( cc ); } +Node TheoryStrings::mkExplain( std::vector< Node >& a ) { + std::vector< Node > an; + return mkExplain( a, an ); +} + Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { std::vector< TNode > antec_exp; for( unsigned i=0; i<a.size(); i++ ){ @@ -1247,6 +1411,61 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) return ant; } +bool TheoryStrings::checkLengths() { + bool addedLemma = false; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ) { + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + //EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); + //get the constant for the equivalence class + //int c_len = ...; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + //if n is concat, and + //if n has not instantiatied the concat..length axiom + //then, add lemma + if( n.getKind() == kind::CONST_STRING ){ //n.getKind() == kind::STRING_CONCAT || + if( d_length_inst.find(n)==d_length_inst.end() ){ + d_length_inst[n] = true; + Trace("strings-debug") << "get n: " << n << endl; + Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); + d_length_intro_vars.push_back( sk ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); + eq = Rewriter::rewrite(eq); + Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl; + d_out->lemma(eq); + Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node lsum; + if( n.getKind() == kind::STRING_CONCAT ){ + //add lemma + std::vector<Node> node_vec; + for( unsigned i=0; i<n.getNumChildren(); i++ ) { + Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } + lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); + }else{ + //add lemma + lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) ); + } + Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); + ceq = Rewriter::rewrite(ceq); + Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl; + d_out->lemma(ceq); + addedLemma = true; + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + return addedLemma; +} + bool TheoryStrings::checkNormalForms() { Trace("strings-process") << "Normalize equivalence classes...." << std::endl; eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); @@ -1257,14 +1476,20 @@ bool TheoryStrings::checkNormalForms() { bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() ); if (print) { eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - Trace("strings-eqc") << "Eqc( " << eqc << " ) : "; + Trace("strings-eqc") << "Eqc( " << eqc << " ) : { "; while( !eqc2_i.isFinished() ) { if( (*eqc2_i)!=eqc ){ Trace("strings-eqc") << (*eqc2_i) << " "; } ++eqc2_i; } - Trace("strings-eqc") << std::endl; + Trace("strings-eqc") << " } " << std::endl; + EqcInfo * ei = getOrMakeEqcInfo( eqc, false ); + if( ei ){ + Trace("strings-eqc-debug") << "* Length term : " << ei->d_length_term.get() << std::endl; + Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei->d_cardinality_lem_k.get() << std::endl; + Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei->d_normalized_length.get() << std::endl; + } } ++eqcs2_i; } @@ -1318,6 +1543,7 @@ bool TheoryStrings::checkNormalForms() { std::vector< Node > nf; std::vector< Node > nf_exp; normalizeEquivalenceClass(eqc, visited, nf, nf_exp); + Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; if( d_conflict ){ return true; }else if ( d_pending.empty() && d_lemma_cache.empty() ){ @@ -1401,6 +1627,42 @@ bool TheoryStrings::checkNormalForms() { } } +bool TheoryStrings::checkLengthsEqc() { + bool addedLemma = false; + std::vector< Node > nodes; + getEquivalenceClasses( nodes ); + for( unsigned i=0; i<nodes.size(); i++ ){ + if( d_normal_forms[nodes[i]].size()>1 ){ + Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl; + //check if there is a length term for this equivalence class + EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false ); + Node lt = ei ? ei->d_length_term : Node::null(); + if( !lt.isNull() ){ + Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + //now, check if length normalization has occurred + if( ei->d_normalized_length.get().isNull() ){ + //if not, add the lemma + std::vector< Node > ant; + ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() ); + ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) ); + Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) ); + lc = Rewriter::rewrite( lc ); + Node eq = llt.eqNode( lc ); + ei->d_normalized_length.set( eq ); + sendLemma( mkExplain( ant ), eq, "Length Normalization" ); + addedLemma = true; + } + } + }else{ + Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl; + } + } + if( addedLemma ){ + doPendingLemmas(); + } + return addedLemma; +} + bool TheoryStrings::checkCardinality() { int cardinality = options::stringCharCardinality(); Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 6b8144d6e..16c3d4876 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -50,6 +50,7 @@ class TheoryStrings : public Theory { bool hasTerm( Node a ); bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); + Node getLengthTerm( Node t ); Node getLength( Node t ); public: @@ -131,6 +132,10 @@ class TheoryStrings : public Theory { /** inferences */ NodeList d_infer; NodeList d_infer_exp; + /** normal forms */ + std::map< Node, Node > d_normal_forms_base; + std::map< Node, std::vector< Node > > d_normal_forms; + std::map< Node, std::vector< Node > > d_normal_forms_exp; //map of pairs of terms that have the same normal form NodeListMap d_nf_pairs; void addNormalFormPair( Node n1, Node n2 ); @@ -179,6 +184,8 @@ class TheoryStrings : public Theory { context::CDO< Node > d_const_term; context::CDO< Node > d_length_term; context::CDO< unsigned > d_cardinality_lem_k; + // 1 = added length lemma + context::CDO< Node > d_normalized_length; }; /** map from representatives to information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; @@ -186,14 +193,14 @@ class TheoryStrings : public Theory { //maintain which concat terms have the length lemma instantiatied std::map< Node, bool > d_length_inst; private: - std::map< Node, std::vector< Node > > d_normal_forms; - std::map< Node, std::vector< Node > > d_normal_forms_exp; - void getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, + bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); - void normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); + bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); + bool checkLengths(); bool checkNormalForms(); + bool checkLengthsEqc(); bool checkCardinality(); bool checkInductiveEquations(); int gcd(int a, int b); @@ -222,8 +229,10 @@ protected: void sendLemma( Node ant, Node conc, const char * c ); void sendSplit( Node a, Node b, const char * c ); /** mkConcat **/ + Node mkConcat( Node n1, Node n2 ); Node mkConcat( std::vector< Node >& c ); /** mkExplain **/ + Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); //get equivalence classes diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8fa4345e5..f303fd333 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -84,7 +84,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret } } -Node StringsPreprocess::simplify( Node t ) { + +Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; @@ -92,21 +93,39 @@ Node StringsPreprocess::simplify( Node t ) { if( t.getKind() == kind::STRING_IN_REGEXP ){ // t0 in t1 + Node t0 = simplify( t[0], new_nodes ); //rewrite it std::vector< Node > ret; - simplifyRegExp( t[0], t[1], ret ); + simplifyRegExp( t0, t[1], ret ); Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); d_cache[t] = (t == n) ? Node::null() : n; return n; - }else if( t.getNumChildren()>0 ){ + }else if( t.getKind() == kind::STRING_SUBSTR ){ + Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" ); + Node x = simplify( t[0], new_nodes ); + Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); + new_nodes.push_back( x_eq_123 ); + Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + new_nodes.push_back( len_sk1_eq_i ); + Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); + new_nodes.push_back( len_sk2_eq_j ); + + d_cache[t] = sk2; + return sk2; + } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { cc.push_back(t.getOperator()); } bool changed = false; for( unsigned i=0; i<t.getNumChildren(); i++ ){ - Node tn = simplify( t[i] ); + Node tn = simplify( t[i], new_nodes ); cc.push_back( tn ); changed = changed || tn!=t[i]; } @@ -125,9 +144,11 @@ Node StringsPreprocess::simplify( Node t ) { } void StringsPreprocess::simplify(std::vector< Node > &vec_node) { + std::vector< Node > new_nodes; for( unsigned i=0; i<vec_node.size(); i++ ){ - vec_node[i] = simplify( vec_node[i] ); + vec_node[i] = simplify( vec_node[i], new_nodes ); } + vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() ); } }/* CVC4::theory::strings namespace */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index f82a3cf24..d07249a02 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -32,7 +32,7 @@ class StringsPreprocess { std::hash_map<TNode, Node, TNodeHashFunction> d_cache; private: void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); - Node simplify( Node t ); + Node simplify( Node t, std::vector< Node > &new_nodes ); public: void simplify(std::vector< Node > &vec_node); }; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 412135675..3a7ad1ee0 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -137,7 +137,20 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - } + } else if(node.getKind() == kind::STRING_SUBSTR) { + if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { + int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { + retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); + } else { + // TODO: some issues, must be guarded by users + retNode = NodeManager::currentNM()->mkConst( false ); + } + } else { + //handled by preprocess + } + } Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, retNode); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 8fc630206..ef8f58f80 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -61,6 +61,28 @@ public: } }; +class StringSubstrTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ){ + TypeNode t = n[0].getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms in substr"); + } + t = n[1].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr"); + } + t = n[2].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr"); + } + } + return nodeManager->stringType(); + } +}; + class RegExpConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 163dd3c1f..8c85e4dd2 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1152,7 +1152,7 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu clique.pop_back(); } //debugging information - if( options::ufssSymBreak() ){ + if( Trace.isOn("uf-ss-cliques") ){ std::vector< Node > clique_vec; clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); addClique( d_cardinality, clique_vec ); diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index b66d1cbe4..682e1e1e7 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -21,6 +21,7 @@ #include "util/sort_inference.h" #include "theory/uf/options.h" +#include "smt/options.h" //#include "theory/rewriter.h" using namespace CVC4; @@ -75,10 +76,11 @@ bool SortInference::UnionFind::isValid() { } -void SortInference::recordSubsort( int s ){ +void SortInference::recordSubsort( TypeNode tn, int s ){ s = d_type_union_find.getRepresentative( s ); if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){ d_sub_sorts.push_back( s ); + d_type_sub_sorts[tn].push_back( s ); } } @@ -91,7 +93,25 @@ void SortInference::printSort( const char* c, int t ){ } } -void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ +void SortInference::reset() { + d_sub_sorts.clear(); + d_non_monotonic_sorts.clear(); + d_type_sub_sorts.clear(); + //reset info + sortCount = 1; + d_type_union_find.clear(); + d_type_types.clear(); + d_id_for_types.clear(); + d_op_return_types.clear(); + d_op_arg_types.clear(); + d_var_types.clear(); + //for rewriting + d_symbol_map.clear(); + d_const_map.clear(); +} + +bool SortInference::simplify( std::vector< Node >& assertions ){ + Trace("sort-inference") << "Calculating sort inference..." << std::endl; //process all assertions for( unsigned i=0; i<assertions.size(); i++ ){ Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl; @@ -100,53 +120,62 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ } for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ Trace("sort-inference") << it->first << " : "; + TypeNode retTn = it->first.getType(); if( !d_op_arg_types[ it->first ].empty() ){ Trace("sort-inference") << "( "; for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){ - recordSubsort( d_op_arg_types[ it->first ][i] ); + recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] ); printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); Trace("sort-inference") << " "; } Trace("sort-inference") << ") -> "; + retTn = retTn[(int)retTn.getNumChildren()-1]; } - recordSubsort( it->second ); + recordSubsort( retTn, it->second ); printSort( "sort-inference", it->second ); Trace("sort-inference") << std::endl; } for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl; - for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - printSort( "sort-inference", it2->second ); + for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){ + recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] ); + printSort( "sort-inference", it->second[it->first[0][i]] ); Trace("sort-inference") << std::endl; } Trace("sort-inference") << std::endl; } - //determine monotonicity of sorts - for( unsigned i=0; i<assertions.size(); i++ ){ - Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl; - std::map< Node, Node > var_bound; - processMonotonic( assertions[i], true, true, var_bound ); - } + if( !options::ufssSymBreak() ){ + bool rewritten = false; + //determine monotonicity of sorts + for( unsigned i=0; i<assertions.size(); i++ ){ + Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl; + std::map< Node, Node > var_bound; + processMonotonic( assertions[i], true, true, var_bound ); + } - Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; - for( unsigned i=0; i<d_sub_sorts.size(); i++ ){ - printSort( "sort-inference", d_sub_sorts[i] ); - if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){ - Trace("sort-inference") << " is interpreted." << std::endl; - }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){ - Trace("sort-inference") << " is monotonic." << std::endl; - }else{ - Trace("sort-inference") << " is not monotonic." << std::endl; + Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; + for( unsigned i=0; i<d_sub_sorts.size(); i++ ){ + printSort( "sort-inference", d_sub_sorts[i] ); + if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){ + Trace("sort-inference") << " is interpreted." << std::endl; + }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){ + Trace("sort-inference") << " is monotonic." << std::endl; + }else{ + Trace("sort-inference") << " is not monotonic." << std::endl; + } } - } - if( doRewrite ){ - //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers) + //simplify all assertions by introducing new symbols wherever necessary for( unsigned i=0; i<assertions.size(); i++ ){ + Node prev = assertions[i]; std::map< Node, Node > var_bound; assertions[i] = simplify( assertions[i], var_bound ); - Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; + if( prev!=assertions[i] ){ + rewritten = true; + Trace("sort-inference-rewrite") << prev << std::endl; + Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; + } } //now, ensure constants are distinct for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ @@ -154,33 +183,79 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ consts.push_back( it2->second ); } - //add lemma enforcing introduced constants to be distinct? + //TODO: add lemma enforcing introduced constants to be distinct } - }else if( !options::ufssSymBreak() ){ - std::map< int, Node > constants; - //just add a bunch of unit lemmas + + //enforce constraints based on monotonicity + for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){ + int nmonSort = -1; + for( unsigned i=0; i<it->second.size(); i++ ){ + if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ + nmonSort = it->second[i]; + break; + } + } + if( nmonSort!=-1 ){ + std::vector< Node > injections; + TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first ); + for( unsigned i=0; i<it->second.size(); i++ ){ + if( it->second[i]!=nmonSort ){ + TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first ); + //make injection to nmonSort + Node a1 = mkInjection( new_tn, base_tn ); + injections.push_back( a1 ); + if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ + //also must make injection from nmonSort to this + Node a2 = mkInjection( base_tn, new_tn ); + injections.push_back( a2 ); + } + } + } + Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl; + for( unsigned j=0; j<injections.size(); j++ ){ + Trace("sort-inference-rewrite") << " " << injections[j] << std::endl; + } + assertions.insert( assertions.end(), injections.begin(), injections.end() ); + if( !injections.empty() ){ + rewritten = true; + } + } + } + //no sub-sort information is stored + reset(); + return rewritten; + } + /* + else if( !options::ufssSymBreak() ){ + //just add the unit lemmas between constants + std::map< TypeNode, std::map< int, Node > > constants; for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ int rt = d_type_union_find.getRepresentative( it->second ); - if( d_op_arg_types[ it->first ].empty() && constants.find( rt )==constants.end() ){ - constants[ rt ] = it->first; + if( d_op_arg_types[ it->first ].empty() ){ + TypeNode tn = it->first.getType(); + if( constants[ tn ].find( rt )==constants[ tn ].end() ){ + constants[ tn ][ rt ] = it->first; + } } } //add unit lemmas for each constant - Node first_const; - for( std::map< int, Node >::iterator it = constants.begin(); it != constants.end(); ++it ){ - if( first_const.isNull() ){ - first_const = it->second; - }else{ - Node eq = first_const.eqNode( it->second ); - //eq = Rewriter::rewrite( eq ); - Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl; - assertions.push_back( eq ); + for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){ + Node first_const; + for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( first_const.isNull() ){ + first_const = it2->second; + }else{ + Node eq = first_const.eqNode( it2->second ); + //eq = Rewriter::rewrite( eq ); + Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl; + assertions.push_back( eq ); + } } } - - } + */ initialSortCount = sortCount; + return false; } void SortInference::setEqual( int t1, int t2 ){ @@ -234,7 +309,7 @@ int SortInference::getIdForType( TypeNode tn ){ } int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ - Trace("sort-inference-debug") << "Process " << n << std::endl; + Trace("sort-inference-debug") << "...Process " << n << std::endl; //add to variable bindings if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ if( d_var_types.find( n )!=d_var_types.end() ){ @@ -284,9 +359,14 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); if( d_op_return_types.find( op )==d_op_return_types.end() ){ - //assign arbitrary sort for return type - d_op_return_types[op] = sortCount; - sortCount++; + if( n.getType().isBoolean() ){ + //use booleans + d_op_return_types[op] = getIdForType( n.getType() ); + }else{ + //assign arbitrary sort for return type + d_op_return_types[op] = sortCount; + sortCount++; + } //d_type_eq_class[sortCount].push_back( op ); //assign arbitrary sort for argument types for( size_t i=0; i<n.getNumChildren(); i++ ){ @@ -306,7 +386,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ Trace("sort-inference-debug") << n << " is a bound variable." << std::endl; //the return type was specified while binding retType = d_var_types[it->second][n]; - }else if( n.getKind() == kind::VARIABLE ){ + }else if( n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM ){ Trace("sort-inference-debug") << n << " is a variable." << std::endl; if( d_op_return_types.find( n )==d_op_return_types.end() ){ //assign arbitrary sort @@ -333,13 +413,14 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ retType = getIdForType( n.getType() ); } } - Trace("sort-inference-debug") << "Type( " << n << " ) = "; + Trace("sort-inference-debug") << "...Type( " << n << " ) = "; printSort("sort-inference-debug", retType ); Trace("sort-inference-debug") << std::endl; return retType; } void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) { + Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl; if( n.getKind()==kind::FORALL ){ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ var_bound[n[0][i]] = n; @@ -351,25 +432,24 @@ void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< N }else if( n.getKind()==kind::EQUAL ){ if( !hasPol || pol ){ for( unsigned i=0; i<2; i++ ){ - if( var_bound.find( n[i] )==var_bound.end() ){ + if( var_bound.find( n[i] )!=var_bound.end() ){ int sid = getSortId( var_bound[n[i]], n[i] ); d_non_monotonic_sorts[sid] = true; break; } } } - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - bool npol = pol; - bool nhasPol = hasPol; - if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){ - npol = !npol; - } - if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){ - nhasPol = false; - } - processMonotonic( n[i], npol, nhasPol, var_bound ); + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + bool npol = pol; + bool nhasPol = hasPol; + if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){ + npol = !npol; } + if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){ + nhasPol = false; + } + processMonotonic( n[i], npol, nhasPol, var_bound ); } } @@ -384,15 +464,14 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){ if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){ retType = pref; }else{ - if( d_subtype_count.find( pref )==d_subtype_count.end() ){ - d_subtype_count[pref] = 0; - } //must create new type std::stringstream ss; - ss << "it_" << d_subtype_count[pref] << "_" << pref; - d_subtype_count[pref]++; + ss << "it_" << t << "_" << pref; retType = NodeManager::currentNM()->mkSort( ss.str() ); } + Trace("sort-inference") << "-> Make type " << retType << " to correspond to "; + printSort("sort-inference", t ); + Trace("sort-inference") << std::endl; d_id_for_types[ retType ] = rt; d_type_types[ rt ] = retType; return retType; @@ -419,6 +498,10 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst??? } return d_const_map[tn][ old ]; + }else if( old.getKind()==kind::BOUND_VARIABLE ){ + std::stringstream ss; + ss << "b_" << old; + return NodeManager::currentNM()->mkBoundVar( ss.str(), tn ); }else{ std::stringstream ss; ss << "i_$$_" << old; @@ -473,7 +556,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ Assert( false ); } } - return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + return NodeManager::currentNM()->mkNode( kind::EQUAL, children ); }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); if( d_symbol_map.find( op )==d_symbol_map.end() ){ @@ -519,7 +602,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ std::map< Node, Node >::iterator it = var_bound.find( n ); if( it!=var_bound.end() ){ return it->second; - }else if( n.getKind() == kind::VARIABLE ){ + }else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){ if( d_symbol_map.find( n )==d_symbol_map.end() ){ TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() ); d_symbol_map[n] = getNewSymbol( n, tn ); @@ -534,6 +617,22 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ } } + +Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { + std::vector< TypeNode > tns; + tns.push_back( tn1 ); + TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 ); + Node f = NodeManager::currentNM()->mkSkolem( "inj_$$", typ, "injection for monotonicity constraint" ); + Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; + Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 ); + Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 ); + return NodeManager::currentNM()->mkNode( kind::FORALL, + NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), + NodeManager::currentNM()->mkNode( kind::IMPLIES, + NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ), + v1.eqNode( v2 ) ) ); +} + int SortInference::getSortId( Node n ) { Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n; if( d_op_return_types.find( op )!=d_op_return_types.end() ){ @@ -554,6 +653,7 @@ int SortInference::getSortId( Node f, Node v ) { void SortInference::setSkolemVar( Node f, Node v, Node sk ){ Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl; if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){ + //calculate the sort for variables if not done so already std::map< Node, Node > var_bound; process( f, var_bound ); } diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index 8f0fc5e9f..cd80f57d8 100644 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -31,7 +31,8 @@ private: //all subsorts std::vector< int > d_sub_sorts; std::map< int, bool > d_non_monotonic_sorts; - void recordSubsort( int s ); + std::map< TypeNode, std::vector< int > > d_type_sub_sorts; + void recordSubsort( TypeNode tn, int s ); public: class UnionFind { public: @@ -79,20 +80,21 @@ private: std::map< Node, Node > d_symbol_map; //mapping from constants to new symbols std::map< TypeNode, std::map< Node, Node > > d_const_map; - //number of subtypes generated - std::map< TypeNode, int > d_subtype_count; //helper functions for simplify TypeNode getOrCreateTypeForId( int t, TypeNode pref ); TypeNode getTypeForId( int t ); Node getNewSymbol( Node old, TypeNode tn ); //simplify Node simplify( Node n, std::map< Node, Node >& var_bound ); - + //make injection + Node mkInjection( TypeNode tn1, TypeNode tn2 ); + //reset + void reset(); public: SortInference() : sortCount( 1 ){} ~SortInference(){} - void simplify( std::vector< Node >& assertions, bool doRewrite = false ); + bool simplify( std::vector< Node >& assertions ); //get sort id for term n int getSortId( Node n ); //get sort id for variable of quantified formula f diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index a1ae66a5f..9b9fdef7a 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -26,15 +26,15 @@ TESTS = \ str004.smt2 \ str005.smt2 \ model001.smt2 \ + substr001.smt2 \ loop001.smt2 \ + loop002.smt2 \ loop003.smt2 \ + loop004.smt2 \ + loop005.smt2 \ + loop006.smt2 \ loop007.smt2 -# loop002.smt2 -# loop004.smt2 -# loop005.smt2 -# loop006.smt2 - FAILING_TESTS = EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/strings/loop001.smt2 b/test/regress/regress0/strings/loop001.smt2 index 11460b335..815acce5c 100644 --- a/test/regress/regress0/strings/loop001.smt2 +++ b/test/regress/regress0/strings/loop001.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2 index 2f96241dc..90492189f 100644 --- a/test/regress/regress0/strings/loop002.smt2 +++ b/test/regress/regress0/strings/loop002.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2 index b4fbcf7d5..1247170c9 100644 --- a/test/regress/regress0/strings/loop003.smt2 +++ b/test/regress/regress0/strings/loop003.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 index 6e5fc96d4..4401ef794 100644 --- a/test/regress/regress0/strings/loop005.smt2 +++ b/test/regress/regress0/strings/loop005.smt2 @@ -1,7 +1,3 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic QF_S) (set-info :status sat) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index 0534d8b53..bea4037d1 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2 index 2832b5c96..ac43afee1 100644 --- a/test/regress/regress0/strings/model001.smt2 +++ b/test/regress/regress0/strings/model001.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (set-option :produce-models true) diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 new file mode 100644 index 000000000..b5ff587b2 --- /dev/null +++ b/test/regress/regress0/strings/substr001.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun i1 () Int)
+(declare-fun i2 () Int)
+(declare-fun i3 () Int)
+(declare-fun i4 () Int)
+
+(assert (= "efg" (str.sub x i1 i2) ) )
+(assert (= "bef" (str.sub x i3 i4) ) )
+(assert (> (str.len x) 5))
+
+(check-sat)
|