summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options2
-rw-r--r--src/smt/smt_engine.cpp10
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h4
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp5
-rw-r--r--src/theory/quantifiers/term_database.cpp27
5 files changed, 37 insertions, 11 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index c27b21e23..74b3011a6 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -210,6 +210,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50
number of ground terms to generate for model filtering
option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
more aggressive merging for universal equality engine, introduces terms
+option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3
+ maximum depth of terms to consider for conjectures
### synthesis options
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bff8e187f..bd67af466 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1095,20 +1095,27 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
}
void SmtEngine::finishInit() {
+ Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
// ensure that our heuristics are properly set up
setDefaults();
+
+ Trace("smt-debug") << "Making decision engine..." << std::endl;
d_decisionEngine = new DecisionEngine(d_context, d_userContext);
d_decisionEngine->init(); // enable appropriate strategies
+ Trace("smt-debug") << "Making prop engine..." << std::endl;
d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
d_userContext, d_private->getReplayLog(),
d_replayStream, d_channels);
+ Trace("smt-debug") << "Setting up theory engine..." << std::endl;
d_theoryEngine->setPropEngine(d_propEngine);
d_theoryEngine->setDecisionEngine(d_decisionEngine);
+ Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
d_theoryEngine->finishInit();
+ Trace("smt-debug") << "Set up assertion list..." << std::endl;
// [MGD 10/20/2011] keep around in incremental mode, due to a
// cleanup ordering issue and Nodes/TNodes. If SAT is popped
// first, some user-context-dependent TNodes might still exist
@@ -1129,6 +1136,7 @@ void SmtEngine::finishInit() {
<< SetBenchmarkLogicCommand(everything.getLogicString());
}
+ Trace("smt-debug") << "Dump declaration commands..." << std::endl;
// dump out any pending declaration commands
for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
Dump("declarations") << *d_dumpCommands[i];
@@ -1137,6 +1145,7 @@ void SmtEngine::finishInit() {
d_dumpCommands.clear();
PROOF( ProofManager::currentPM()->setLogic(d_logic); );
+ Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
}
void SmtEngine::finalOptionsAreSet() {
@@ -3638,6 +3647,7 @@ Result SmtEngine::check() {
// Make sure the prop layer has all of the assertions
Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
d_private->processAssertions();
+ Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
// Turn off stop only for QF_LRA
// TODO: Bring up in a meeting where to put this
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index cd31778ec..dd2803d30 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -260,10 +260,6 @@ public:
/** get instantiate cons */
static Node getInstCons( Node n, const Datatype& dt, int index ) {
Assert( index>=0 && index<(int)dt.getNumConstructors() );
- Type tspec;
- if( dt.isParametric() ){
- tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
- }
std::vector< Node > children;
children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 27bbb0f5f..2cc49ef5a 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -605,7 +605,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
std::vector< TypeNode > rt_types;
std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs;
unsigned addedLemmas = 0;
- for( unsigned depth=1; depth<=3; depth++ ){
+ unsigned maxDepth = options::conjectureGenMaxDepth();
+ for( unsigned depth=1; depth<=maxDepth; depth++ ){
Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl;
Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl;
//set up environment
@@ -1167,6 +1168,8 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi
d_waiting_conjectures_score.push_back( score );
d_waiting_conjectures[lhs].push_back( rhs );
d_waiting_conjectures[rhs].push_back( lhs );
+ }else{
+ Trace("sg-conjecture-debug2") << "...do not consider " << lhs << " == " << rhs << ", score = " << score << std::endl;
}
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 51c72d7bb..8b09d8e5d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1016,14 +1016,29 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
}
-void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
+void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
+ TypeNode tspec;
+ if( dt.isParametric() ){
+ tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) );
+ Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl;
+ Assert( tspec.getNumChildren()==dc.getNumArgs() );
+ }
+ Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl;
for( unsigned j=0; j<dc.getNumArgs(); j++ ){
- TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
std::vector< Node > ssc;
- if( tn==ntn ){
- ssc.push_back( n );
+ if( dt.isParametric() ){
+ Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl;
+ if( tspec[j]==ntn ){
+ ssc.push_back( n );
+ }
+ }else{
+ TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
+ Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
+ if( tn==ntn ){
+ ssc.push_back( n );
+ }
}
- /* TODO
+ /* TODO: more than weak structural induction
else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
visited.push_back( tn );
const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
@@ -1101,7 +1116,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
std::vector< Node > disj;
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
std::vector< Node > selfSel;
- getSelfSel( dt[i], k, tn, selfSel );
+ getSelfSel( dt, dt[i], k, tn, selfSel );
std::vector< Node > conj;
conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
for( unsigned j=0; j<selfSel.size(); j++ ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback