Disambiguate namespaces in options, fix permissions

diff --git a/src/main/options b/src/main/options
index 18cc08ed78e0cd67446e073bcad1c1b23111c1ae..f523ea499ca3a7777b8fddd92e2f0ac16c7707b0 100644 (file)
--- 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 8189d61f8e3bae5999a6b60578c5cfe474bc2ac6..65bb44de6d21338ed2302253fbfbbcc488860b6f 100644 (file)
--- 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 a5b97712140993f7ee157a5ae73f54bcb3333720..596d46c54ad4f98dbde5dc2210251c5ab2ed3cc7 100644 (file)
--- 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 (executable)
new mode 100644 (file)

diff --git a/test/regress/regress0/fmf/fore19-exp2-core.smt2 b/test/regress/regress0/fmf/fore19-exp2-core.smt2
old mode 100755 (executable)
new mode 100644 (file)

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 (executable)
new mode 100644 (file)