summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/boolean_terms.cpp4
-rw-r--r--src/smt/boolean_terms.h2
-rw-r--r--src/smt/command_list.cpp2
-rw-r--r--src/smt/command_list.h2
-rw-r--r--src/smt/logic_exception.h2
-rw-r--r--src/smt/logic_request.cpp17
-rw-r--r--src/smt/logic_request.h4
-rw-r--r--src/smt/modal_exception.h2
-rw-r--r--src/smt/model_postprocessor.cpp2
-rw-r--r--src/smt/model_postprocessor.h2
-rw-r--r--src/smt/options_handlers.h4
-rw-r--r--src/smt/simplification_mode.cpp2
-rw-r--r--src/smt/simplification_mode.h2
-rw-r--r--src/smt/smt_engine.cpp105
-rw-r--r--src/smt/smt_engine.h9
-rw-r--r--src/smt/smt_engine_check_proof.cpp2
-rw-r--r--src/smt/smt_engine_scope.cpp2
-rw-r--r--src/smt/smt_engine_scope.h2
-rw-r--r--src/smt/smt_options_template.cpp2
19 files changed, 98 insertions, 71 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index c779af4ff..df5499c86 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index bdd9ff839..ed676c667 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp
index fca714490..18a09e7ed 100644
--- a/src/smt/command_list.cpp
+++ b/src/smt/command_list.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/command_list.h b/src/smt/command_list.h
index ac0c382be..47185b365 100644
--- a/src/smt/command_list.h
+++ b/src/smt/command_list.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
index 02c293ab4..8fda9b9e2 100644
--- a/src/smt/logic_exception.h
+++ b/src/smt/logic_exception.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp
index a0b6d2bb9..09559eb8d 100644
--- a/src/smt/logic_request.cpp
+++ b/src/smt/logic_request.cpp
@@ -1,3 +1,20 @@
+/********************* */
+/*! \file logic_request.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
#include "smt/logic_request.h"
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 8aad440c6..94c6c2a5e 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -1,9 +1,9 @@
/********************* */
/*! \file logic_request.h
** \verbatim
- ** Original author: Morgan Deters
+ ** Original author: Martin Brain <>
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
diff --git a/src/smt/modal_exception.h b/src/smt/modal_exception.h
index bf463bb05..11e78ab19 100644
--- a/src/smt/modal_exception.h
+++ b/src/smt/modal_exception.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 5a14924ff..eea8d2282 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
index 952bb1bf0..024f4f3a3 100644
--- a/src/smt/model_postprocessor.h
+++ b/src/smt/model_postprocessor.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index af8e8663c..61e17801d 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): Clark Barrett, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp
index d3155313f..f728fa862 100644
--- a/src/smt/simplification_mode.cpp
+++ b/src/smt/simplification_mode.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h
index 6023bf518..2242e8bdf 100644
--- a/src/smt/simplification_mode.h
+++ b/src/smt/simplification_mode.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ab805a6c5..7c5f98253 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Tianyi Liang, Christopher L. Conway, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds
+ ** Minor contributors (to current version): Christopher L. Conway, Tianyi Liang, Martin Brain <>, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -528,7 +528,7 @@ public:
/**
* Expand definitions in n.
*/
- Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
+ Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false)
throw(TypeCheckingException, LogicException);
/**
@@ -872,12 +872,14 @@ void SmtEngine::setDefaults() {
}
// set strings-exp
+ /* - disabled for 1.4 release [MGD 2014.06.25]
if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
if(! options::stringExp.wasSetByUser()) {
options::stringExp.set( true );
Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
}
}
+ */
// for strings
if(options::stringExp()) {
if( !d_logic.isQuantified() ) {
@@ -891,6 +893,9 @@ void SmtEngine::setDefaults() {
Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
}
if(! options::fmfBoundInt.wasSetByUser()) {
+ if(! options::fmfBoundIntLazy.wasSetByUser()) {
+ options::fmfBoundIntLazy.set( true );
+ }
options::fmfBoundInt.set( true );
Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
}
@@ -927,44 +932,6 @@ void SmtEngine::setDefaults() {
}
}
- // set strings-exp
- if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS)) {
- if(! options::stringExp.wasSetByUser()) {
- options::stringExp.set(true);
- Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
- }
- }
- // for strings
- if(options::stringExp()) {
- if( !d_logic.isQuantified() ) {
- d_logic = d_logic.getUnlockedCopy();
- d_logic.enableQuantifiers();
- d_logic.lock();
- Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
- }
- if(! options::finiteModelFind.wasSetByUser()) {
- options::finiteModelFind.set( true );
- Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
- }
- if(! options::fmfBoundInt.wasSetByUser()) {
- if(! options::fmfBoundIntLazy.wasSetByUser()) {
- options::fmfBoundIntLazy.set( true );
- }
- options::fmfBoundInt.set( true );
- Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
- }
- /*
- if(! options::rewriteDivk.wasSetByUser()) {
- options::rewriteDivk.set( true );
- Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
- }*/
- /*
- if(! options::stringFMF.wasSetByUser()) {
- options::stringFMF.set( true );
- Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
- }
- */
- }
// by default, symmetry breaker is on only for QF_UF
if(! options::ufSymmetryBreaker.wasSetByUser()) {
bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
@@ -1064,14 +1031,23 @@ void SmtEngine::setDefaults() {
// Unconstrained simp currently does *not* support model generation
if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
if (options::produceModels()) {
+ if (options::produceModels.wasSetByUser()) {
+ throw OptionException("Cannot use unconstrained-simp with model generation.");
+ }
Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl;
setOption("produce-models", SExpr("false"));
}
if (options::produceAssignments()) {
+ if (options::produceAssignments.wasSetByUser()) {
+ throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
+ }
Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl;
setOption("produce-assignments", SExpr("false"));
}
if (options::checkModels()) {
+ if (options::checkModels.wasSetByUser()) {
+ throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
+ }
Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl;
setOption("check-models", SExpr("false"));
}
@@ -1501,10 +1477,7 @@ void SmtEngine::defineFunction(Expr func,
d_definedFunctions->insert(funcNode, def);
}
-
-
-
-Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
+Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
throw(TypeCheckingException, LogicException) {
stack< triple<Node, Node, bool> > worklist;
@@ -1586,12 +1559,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
n.begin(), n.end());
Debug("expand") << "made : " << instance << endl;
- Node expanded = expandDefinitions(instance, cache);
+ Node expanded = expandDefinitions(instance, cache, expandOnly);
cache[n] = (n == expanded ? Node::null() : expanded);
result.push(expanded);
continue;
- } else {
+ } else if(! expandOnly) {
+ // do not do any theory stuff if expandOnly is true
+
theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
Assert(t != NULL);
@@ -3017,7 +2992,12 @@ void SmtEnginePrivate::processAssertions() {
if( options::sortInference() ){
//sort inference technique
- d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
+ SortInference * si = d_smt.d_theoryEngine->getSortInference();
+ si->simplify( d_assertionsToPreprocess );
+ for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
+ d_smt.setPrintFuncInModel( it->first.toExpr(), false );
+ d_smt.setPrintFuncInModel( it->second.toExpr(), true );
+ }
}
//if( options::quantConflictFind() ){
@@ -3176,8 +3156,11 @@ void SmtEnginePrivate::processAssertions() {
// everything gets bit-blasted to internal SAT solver
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]);
+ TNode atom = d_assertionsToCheck[i];
+ Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
d_assertionsToCheck[i] = eager_atom;
+ TheoryModel* m = d_smt.d_theoryEngine->getModel();
+ m->addSubstitution(eager_atom, atom);
}
}
@@ -3473,7 +3456,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
Dump("benchmark") << ExpandDefinitionsCommand(e);
}
hash_map<Node, Node, NodeHashFunction> cache;
- Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+ Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
n = postprocess(n, TypeNode::fromType(e.getType()));
return n.toExpr();
@@ -4120,4 +4103,26 @@ void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
d_theoryEngine->setUserAttribute(attr, expr.getNode());
}
+void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
+ Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
+ for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
+ Command * c = d_modelGlobalCommands[i];
+ DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+ if(dfc != NULL) {
+ if( dfc->getFunction()==f ){
+ dfc->setPrintInModel( p );
+ }
+ }
+ }
+ for( unsigned i=0; i<d_modelCommands->size(); i++ ){
+ Command * c = (*d_modelCommands)[i];
+ DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+ if(dfc != NULL) {
+ if( dfc->getFunction()==f ){
+ dfc->setPrintInModel( p );
+ }
+ }
+ }
+}
+
}/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 72237ff1c..71b42534a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds, Tim King, Clark Barrett, Christopher L. Conway, Kshitij Bansal, Dejan Jovanovic
+ ** Minor contributors (to current version): Martin Brain <>, Tim King, Clark Barrett, Christopher L. Conway, Andrew Reynolds, Kshitij Bansal, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -653,6 +653,11 @@ public:
*/
void setUserAttribute(const std::string& attr, Expr expr);
+ /**
+ * Set print function in model
+ */
+ void setPrintFuncInModel(Expr f, bool p);
+
};/* class SmtEngine */
}/* CVC4 namespace */
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 4c218b48c..2080c772a 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 5a075280d..25004c85e 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 2389181b5..54b9fa1d0 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 987d2e3c7..376584636 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback