From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 4 Jun 2018 18:58:14 +0000 (-0500)
Subject: Enable cegqi (with model values) for floating point by default (#2023)
X-Git-Tag: cvc5-1.0.0~4980
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db491e2e8100101f30e3f211a3c5da55686f7d27;p=cvc5.git

Enable cegqi (with model values) for floating point by default (#2023)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9d10e72be..2836f73b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2071,11 +2071,15 @@ void SmtEngine::setDefaults() {
   }
   //counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
-  if( d_logic.isQuantified() && 
-      ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL &&
-          ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
-        d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) ||
-        options::cbqiAll() ) ){
+  if (d_logic.isQuantified()
+      && ((options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL
+           && (d_logic.isTheoryEnabled(THEORY_ARITH)
+               || d_logic.isTheoryEnabled(THEORY_DATATYPES)
+               || d_logic.isTheoryEnabled(THEORY_BV)
+               || d_logic.isTheoryEnabled(THEORY_FP)))
+          || d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)
+          || options::cbqiAll()))
+  {
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
     }
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 496066ebc..574f2e0f0 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -980,6 +980,7 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
     preRewriteTable[kind::VARIABLE] = rewrite::variable;
     preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
     preRewriteTable[kind::SKOLEM] = rewrite::variable;
+    preRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
 
     preRewriteTable[kind::EQUAL] = rewrite::equal;
 
@@ -1062,6 +1063,7 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
     postRewriteTable[kind::VARIABLE] = rewrite::variable;
     postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
     postRewriteTable[kind::SKOLEM] = rewrite::variable;
+    postRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
 
     postRewriteTable[kind::EQUAL] = rewrite::equal;
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 9dd0bdb04..b18ebcdce 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -153,7 +153,8 @@ CegHandledStatus CegInstantiator::isCbqiKind(Kind k)
 
   // CBQI typically works for satisfaction-complete theories
   TheoryId t = kindToTheoryId(k);
-  if (t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL)
+  if (t == THEORY_BV || t == THEORY_FP || t == THEORY_DATATYPES
+      || t == THEORY_BOOL)
   {
     return CEG_HANDLED;
   }
@@ -221,7 +222,8 @@ CegHandledStatus CegInstantiator::isCbqiSort(
     return itv->second;
   }
   CegHandledStatus ret = CEG_UNHANDLED;
-  if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector())
+  if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector()
+      || tn.isFloatingPoint())
   {
     ret = CEG_HANDLED;
   }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 2eaa6fb81..2ac299177 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1259,6 +1259,7 @@ REG1_TESTS = \
 	regress1/quantifiers/ext-ex-deq-trigger.smt2 \
 	regress1/quantifiers/extract-nproc.smt2 \
 	regress1/quantifiers/florian-case-ax.smt2 \
+	regress1/quantifiers/fp-cegqi-unsat.smt2 \
 	regress1/quantifiers/gauss_init_0030.fof.smt2 \
 	regress1/quantifiers/horn-simple.smt2 \
 	regress1/quantifiers/inst-max-level-segf.smt2 \
diff --git a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
new file mode 100644
index 000000000..1ee8e6c11
--- /dev/null
+++ b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: symfpu
+(set-info :smt-lib-version 2.6)
+(set-logic FP)
+(set-info :status unsat)
+(declare-fun c_main_~E0~7 () (_ FloatingPoint 11 53))
+(declare-fun c_main_~S~7 () (_ FloatingPoint 11 53))
+(assert (and (= ((_ to_fp 11 53) RNE (_ bv0 32)) c_main_~S~7) (fp.geq c_main_~E0~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (fp.leq c_main_~E0~7 ((_ to_fp 11 53) RNE 1.0))))
+(assert (not (and (exists ((main_~E0~7 (_ FloatingPoint 11 53)) (main_~E1~7 (_ FloatingPoint 11 53))) (and (fp.geq main_~E1~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (= c_main_~S~7 (fp.sub RNE (fp.add RNE (fp.mul RNE ((_ to_fp 11 53) RNE 0.999) ((_ to_fp 11 53) RNE (_ bv0 32))) main_~E0~7) main_~E1~7)) (fp.geq main_~E0~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (fp.leq main_~E0~7 ((_ to_fp 11 53) RNE 1.0)) (fp.leq main_~E1~7 ((_ to_fp 11 53) RNE 1.0)))) (fp.geq c_main_~E0~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (fp.leq c_main_~E0~7 ((_ to_fp 11 53) RNE 1.0)))))
+(check-sat)
+(exit)