From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Oct 2017 23:18:35 +0000 (-0500)
Subject: SyGuS term size limit (#1262)
X-Git-Tag: cvc5-1.0.0~5546
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=278b60971f6209ffc0eb76a23548c081dc8c9c56;p=cvc5.git

SyGuS term size limit (#1262)

* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.

* Apply clang format.
---

diff --git a/src/options/datatypes_options b/src/options/datatypes_options
index d4d3e941c..5163cf35d 100644
--- a/src/options/datatypes_options
+++ b/src/options/datatypes_options
@@ -47,5 +47,7 @@ option sygusFair --sygus-fair=MODE CVC4::theory::SygusFairMode :default CVC4::th
   if and how to apply fairness for sygus
 option sygusFairMax --sygus-fair-max bool :default true
   use max instead of sum for multi-function sygus conjectures
+option sygusAbortSize --sygus-abort-size=N int :default -1
+  tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)
   
 endmodule
diff --git a/src/options/uf_options b/src/options/uf_options
index 7e1cbdb17..c93ccf864 100644
--- a/src/options/uf_options
+++ b/src/options/uf_options
@@ -22,7 +22,7 @@ option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
 option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
  apply symmetry breaking for totality axioms
 option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
- tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
+ tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)
 option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
  use explained clique lemmas for uf strong solver
 option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 5d48c1ce2..4999114eb 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1347,6 +1347,12 @@ Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDat
   if( options::sygusFair()!=SYGUS_FAIR_NONE ){
     std::map< unsigned, Node >::iterator it = d_lits.find( s );
     if( it==d_lits.end() ){
+      if (options::sygusAbortSize() != -1 &&
+          static_cast<int>(s) > options::sygusAbortSize()) {
+        Message() << "Maximum term size (" << options::sygusAbortSize()
+                  << ") for enumerative SyGuS exceeded." << std::endl;
+        exit(1);
+      }
       Assert( !d_this.isNull() );
       Node c = NodeManager::currentNM()->mkConst( Rational( s ) );
       Node lit = NodeManager::currentNM()->mkNode( DT_SYGUS_BOUND, d_this, c );
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index e7efba325..4b6a326cf 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1157,8 +1157,10 @@ void SortModel::allocateCardinality( OutputChannel* out ){
   }while( increment );
 
   //check for abort case
-  if( options::ufssAbortCardinality()==d_aloc_cardinality ){
-    Message() << "Maximum cardinality reached." << std::endl;
+  if (options::ufssAbortCardinality() != -1 &&
+      d_aloc_cardinality >= options::ufssAbortCardinality()) {
+    Message() << "Maximum cardinality (" << options::ufssAbortCardinality()
+              << ")  for finite model finding exceeded." << std::endl;
     exit( 1 );
   }else{
     if( applyTotality( d_aloc_cardinality ) ){