From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 May 2013 22:40:34 +0000 (-0500)
Subject: Add support for --dump-models option, in preparation for casc.
X-Git-Tag: cvc5-1.0.0~7287^2~113^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12a1b56a7a6573ae5af47e9d9d6e757e70a6b7a1;p=cvc5.git

Add support for --dump-models option, in preparation for casc.
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index f1742b549..556e51216 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -19,6 +19,8 @@
 
 #include "main/main.h"
 
+#include "smt/options.h"
+
 namespace CVC4 {
 namespace main {
 
@@ -64,6 +66,17 @@ bool CommandExecutor::doCommandSingleton(Command *cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
+  //dump the model if option is set
+  if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
+    CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
+    if(cs != NULL) {
+      if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
+         (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
+        Command * gm = new GetModelCommand;
+        status = doCommandSingleton(gm);
+      }
+    }
+  }
   return status;
 }
 
diff --git a/src/smt/options b/src/smt/options
index 2680f4105..e5f9c2eaf 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -24,6 +24,8 @@ common-option produceModels produce-models -m --produce-models bool :default fal
  support the get-value and get-model commands
 option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
+option dumpModels --dump-models bool :default false
+ output models after every SAT/INVALID/UNKNOWN response
 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on proof generation
 # this is just a placeholder for later; it doesn't show up in command-line options listings