LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.

ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers.  In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.

2 files changed, 9 insertions, 0 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5b71e5ec5..58270b4d0 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -247,6 +247,10 @@ void PropEngine::pop() {
   Debug("prop") << "pop()" << endl;
 }
 
+unsigned PropEngine::getAssertionLevel() const {
+  return d_satSolver->getAssertionLevel();
+}
+
 bool PropEngine::isRunning() const {
   return d_inCheckSat;
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 9e49cf3f1..603cdb0e6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -246,6 +246,11 @@ public:
   void pop();
 
   /**
+   * Get the assertion level of the SAT solver.
+   */
+  unsigned getAssertionLevel() const;
+
+  /**
    * Return true if we are currently searching (either in this or
    * another thread).
    */