From: Tim King <taking@cs.nyu.edu>
Date: Sat, 29 Sep 2012 20:42:16 +0000 (+0000)
Subject: Calling the setIncompleteness() flag on all full checks once a non-linear term has... 
X-Git-Tag: cvc5-1.0.0~7760
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c89b0605d5ff327f140f3b0be87796f086228640;p=cvc5.git

Calling the setIncompleteness() flag on all full checks once a non-linear term has been seen.
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e552ae5a0..2b0d9149d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -58,7 +58,7 @@ const uint32_t RESET_START = 2;
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
-  d_nlIncomplete(u, false),
+  d_nlIncomplete( false),
   d_qflraStatus(Result::SAT_UNKNOWN),
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
@@ -1707,6 +1707,10 @@ void TheoryArith::check(Effort effortLevel){
       }
     }
   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
+  if(fullEffort(effortLevel) && d_nlIncomplete){
+    // TODO this is total paranoia
+    d_out->setIncomplete();
+  }
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
   if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1c2c942fd..4b3a633cb 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -64,7 +64,9 @@ class InstantiatorTheoryArith;
 class TheoryArith : public Theory {
   friend class InstantiatorTheoryArith;
 private:
-  context::CDO<bool> d_nlIncomplete;
+  bool d_nlIncomplete;
+  // TODO A better would be:
+  //context::CDO<bool> d_nlIncomplete;
 
   enum Result::Sat d_qflraStatus;
   // check()