Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

1 files changed, 29 insertions, 0 deletions

diff --git a/test/regress/regress0/quantifiers/set3.smt2 b/test/regress/regress0/quantifiers/set3.smt2
new file mode 100644
index 000000000..d3e51d996
--- /dev/null
+++ b/test/regress/regress0/quantifiers/set3.smt2
@@ -0,0 +1,29 @@
+(set-logic AUFLIA)
+(set-info :source | Assertion verification of simple set manipulation programs. |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Set 0)
+(declare-fun member (Int Set) Bool)
+(declare-fun insert (Set Int) Set)
+(declare-fun delete (Set Int) Set)
+(declare-fun sup (Set) Int)
+(assert (forall ((?x Int) (?s Set)) (member ?x (insert ?s ?x))))
+(assert (forall ((?x Int) (?y Int) (?s Set)) (=> (not (= ?x ?y)) (= (member ?x (insert ?s ?y)) (member ?x ?s)))))
+(assert (forall ((?x Int) (?s Set)) (=> (not (member ?x ?s)) (= (delete ?s ?x) ?s))))
+(assert (forall ((?x Int) (?s Set)) (= (delete (insert ?s ?x) ?x) (delete ?s ?x))))
+(assert (forall ((?x Int) (?y Int) (?s Set)) (=> (not (= ?x ?y)) (= (delete (insert ?s ?y) ?x) (insert (delete ?s ?x) ?y)))))
+(assert (forall ((?s Set)) (member (sup ?s) ?s)))
+(assert (forall ((?s Set) (?x Int)) (=> (member ?x ?s) (<= ?x (sup ?s)))))
+(assert (forall ((?s Set) (?x Int)) (=> (< (sup ?s) ?x) (= (sup (insert ?s ?x)) ?x))))
+(declare-fun arr () (Array Int Int))
+(declare-fun s0 () Set)
+(assert (forall ((?i Int)) (=> (> ?i 0) (< (select arr ?i) (sup s0)))))
+(declare-fun i1 () Int)
+(declare-fun s1 () Set)
+(declare-fun g (Int) Int)
+(assert (forall ((?i Int)) (> (g ?i) 0)))
+(assert (= s1 (insert s0 (select arr (g i1)))))
+(assert (not (= (sup s1) (sup s0))))
+(check-sat)
+(exit)