Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.

2 files changed, 38 insertions, 3 deletions

diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 3a3a097bd..31f99905c 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -23,16 +23,16 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	length_trick.smt2 \
-	length_trick2.smt2 \
 	length_gen_020.smt2 \
 	datatypes.smt2 \
 	datatypes_sat.smt2 \
 	reachability_back_to_the_future.smt2 \
 	relation.smt2 \
 	simulate_rewriting.smt2 \
-	native_arrays.smt2
+	native_arrays.smt2 \
+	read5.smt2
 
-# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
+# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress0/rewriterules/read5.smt2
new file mode 100755
index 000000000..e66df7c7e
--- /dev/null
+++ b/test/regress/regress0/rewriterules/read5.smt2
@@ -0,0 +1,35 @@
+(set-logic AUF)
+(set-info :source |
+Translated from old SVC processor verification benchmarks.  Contact Clark
+Barrett at barrett@cs.nyu.edu for more information.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index)
+(declare-fun a () Index)
+(declare-fun aaa () Index)
+(declare-fun aa () Index)
+(declare-fun S () Arr)
+(declare-fun vvv () Element)
+(declare-fun v () Element)
+(declare-fun vv () Element)
+(declare-fun bbb () Index)
+(declare-fun www () Element)
+(declare-fun bb () Index)
+(declare-fun ww () Element)
+(declare-fun b () Index)
+(declare-fun w () Element)
+(declare-fun SS () Arr)
+(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false))))
+; rewrite rule definition of arrays theory
+(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule)))
+(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule)))
+(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule)))
+(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule)))
+(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat)
+(exit)