From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 5 May 2017 22:41:18 +0000 (-0500)
Subject: Do not eliminate extended arithmetic symbols when finite model finding is on, add... 
X-Git-Tag: cvc5-1.0.0~5809
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4b158635255affcafe52c7664fc5de4660c3f83;p=cvc5.git

Do not eliminate extended arithmetic symbols when finite model finding is on, add regression.
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index a5ecc8e72..f15723e08 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -54,7 +54,7 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
-option elimExtArithQuant --elim-ext-arith-quant bool :default true
+option elimExtArithQuant --elim-ext-arith-quant bool :read-write :default true
  eliminate extended arithmetic symbols in quantified formulas
 option condRewriteQuant --cond-rewrite-quant bool :default true
  conditional rewriting of quantified formulas
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 16da6691c..4e75a7937 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1781,11 +1781,15 @@ void SmtEngine::setDefaults() {
     if( !options::quantDynamicSplit.wasSetByUser() ){
       options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT );
     }
+    //do not eliminate extended arithmetic symbols from quantified formulas
+    if( !options::elimExtArithQuant.wasSetByUser() ){
+      options::elimExtArithQuant.set( false );
+    }
     if( !options::eMatching.wasSetByUser() ){
       options::eMatching.set( options::fmfInstEngine() );
     }
     if( !options::instWhenMode.wasSetByUser() ){
-      //instantiate only on last call  FIXME: remove?
+      //instantiate only on last call
       if( options::eMatching() ){
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 593cdfa8b..b02443989 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -73,7 +73,8 @@ TESTS =	\
 	constr-ground-to.smt2 \
 	bug-041417-set-options.cvc \
 	alg202+1.smt2 \
-	fmf-fun-no-elim-ext-arith.smt2
+	fmf-fun-no-elim-ext-arith.smt2 \
+	fmf-fun-no-elim-ext-arith2.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
new file mode 100644
index 000000000..ea5a5e4b7
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
+    or
+    (= n1 n 0)
+    (= n2 n 0)
+    (
+        and
+        (> n1 0)
+        (> n2 0)
+        (>= n 0)
+        (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0))))
+        (int-and (div n 2) (div n1 2) (div n2 2))
+    )
+))
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= x 1))
+(assert (= y 1))
+(assert (= z 1))
+(assert (int-and z x y))
+(check-sat)