From: Clark Barrett <clarkbarrett@google.com>
Date: Tue, 28 Apr 2015 00:43:10 +0000 (-0700)
Subject: Disambiguate namespaces in options, fix permissions
X-Git-Tag: cvc5-1.0.0~6338
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91cd90ae485a159799d82f7341438a4e9a12a72d;p=cvc5.git

Disambiguate namespaces in options, fix permissions
---

diff --git a/src/main/options b/src/main/options
index 18cc08ed7..f523ea499 100644
--- a/src/main/options
+++ b/src/main/options
@@ -24,7 +24,7 @@ expert-option earlyExit --early-exit bool :default true
  do not run destructors at exit; default on except in debug builds
 
 # portfolio options
-option threads --threads=N unsigned :default 2 :predicate greater(0)
+option threads --threads=N unsigned :default 2 :predicate options::greater(0)
  Total number of threads for portfolio
 option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h"
  configures portfolio thread N (0..#threads-1)
diff --git a/src/prop/options b/src/prop/options
index 8189d61f8..65bb44de6 100644
--- a/src/prop/options
+++ b/src/prop/options
@@ -5,18 +5,18 @@
 
 module PROP "prop/options.h" SAT layer
 
-option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0)
+option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate options::greater_equal(0.0) options::less_equal(1.0)
  sets the frequency of random decisions in the sat solver (P=0.0 by default)
 option satRandomSeed random-seed --random-seed=S uint32_t :default 0 :read-write
  sets the random seed for the sat solver
 
-option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0)
+option satVarDecay double :default 0.95 :predicate options::less_equal(1.0) options::greater_equal(0.0)
  variable activity decay factor for Minisat
-option satClauseDecay double :default 0.999 :predicate less_equal(1.0) greater_equal(0.0)
+option satClauseDecay double :default 0.999 :predicate options::less_equal(1.0) options::greater_equal(0.0)
  clause activity decay factor for Minisat
 option satRestartFirst --restart-int-base=N unsigned :default 25
  sets the base restart interval for the sat solver (N=25 by default)
-option satRestartInc --restart-int-inc=F double :default 3.0 :predicate greater_equal(0.0)
+option satRestartInc --restart-int-inc=F double :default 3.0 :predicate options::greater_equal(0.0)
  sets the restart interval increase factor for the sat solver (F=3.0 by default)
 
 option sat_refine_conflicts --refine-conflicts bool :default false
diff --git a/src/theory/strings/options b/src/theory/strings/options
index a5b977121..596d46c54 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -11,7 +11,7 @@ option stringExp strings-exp --strings-exp bool :default false :read-write
 option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h"
  the strategy of LB rule application: 0-lazy, 1-eager, 2-no
 
-option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
+option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h"
  the alphabet contains only characters from the standard ASCII or the extended one
 
 option stringFMF strings-fmf --strings-fmf bool :default false :read-write
diff --git a/test/regress/regress0/fmf/fib-core.smt2 b/test/regress/regress0/fmf/fib-core.smt2
old mode 100755
new mode 100644
diff --git a/test/regress/regress0/fmf/fore19-exp2-core.smt2 b/test/regress/regress0/fmf/fore19-exp2-core.smt2
old mode 100755
new mode 100644
diff --git a/test/regress/regress0/fmf/with-ind-104-core.smt2 b/test/regress/regress0/fmf/with-ind-104-core.smt2
old mode 100755
new mode 100644