using System.Text;
namespace SynatxHighlighterTest
{
public sealed class KeywordsExample
{
public SolverStats stats;
internal SATHook hook;
internal SolverParams parameters;
private int unique_id; //the unique id seen so far for the nodes
private IntVector active_area;
//private Process currentProcess = Process.GetCurrentProcess();
internal VarVector variables = new VarVector(4);
internal ClsVector clauses = new ClsVector(4);
private ObjVector watched_clauses = new ObjVector(4);
private IntVector free_clauses = new IntVector(4);
public void ForEachMethod()
{
// An array of integers
int[] array1 = { 0, 1, 2, 3, 4, 5 };
foreach (int n in array1)
{
System.Console.WriteLine(n.ToString());
}
// An array of strings
string[] array2 = { "hello", "world" };
foreach (string s in array2)
{
System.Console.WriteLine(s);
}
}
public void ForMethod()
{
// An array of integers
int[] array1 = { 0, 1, 2, 3, 4, 5 };
for (int i = 0; i < 6; i++)
{
System.Console.WriteLine(array1[i].ToString());
}
// An array of strings
string[] array2 = { "hello", "world" };
for (int i = 0; i < 2; i++)
{
System.Console.WriteLine(array2[i]);
}
}
public void WhileMethod()
{
// An array of integers
int[] array1 = { 0, 1, 2, 3, 4, 5 };
int x = 0;
while (x < 6)
{
System.Console.WriteLine(array1[x].ToString());
x++;
}
// An array of strings
string[] array2 = { "hello", "world" };
int y = 0;
while (y < 2)
{
System.Console.WriteLine(array2[y]);
y++;
}
}
public void DoWhileMethod()
{
// An array of integers
int[] array1 = { 0, 1, 2, 3, 4, 5 };
int x = 0;
do
{
System.Console.WriteLine(array1[x].ToString());
x++;
} while (x < 6);
// An array of strings
string[] array2 = { "hello", "world" };
int y = 0;
do
{
System.Console.WriteLine(array2[y]);
y++;
} while (y < 2);
}
public void ForWithBreakMethod()
{
for (int counter = 1; counter <= 1000; counter++)
{
if (counter == 10)
break;
System.Console.WriteLine(counter);
}
}
public void ForEachWithInMethod()
{
int[] fibarray = new int[] { 0, 1, 2, 3, 5, 8, 13 };
foreach (int i in fibarray)
{
System.Console.WriteLine(i);
}
}
public void SwitchMethod()
{
int caseSwitch = 1;
switch (caseSwitch)
{
case 1:
Console.WriteLine("Case 1");
break;
case 2:
Console.WriteLine("Case 2");
break;
default:
Console.WriteLine("Default case");
break;
}
}
public void IfElseMethod()
{
bool flagCheck = true;
if (flagCheck == true)
{
Console.WriteLine("The flag is set to true.");
}
else
{
Console.WriteLine("The flag is set to false.");
}
}
internal short m_value;
//| <include path='docs/doc[@for="Int16.MaxValue"]/*' />
public const short MaxValue = (short)0x7FFF;
//| <include path='docs/doc[@for="Int16.MinValue"]/*' />
public const short MinValue = unchecked((short)0x8000);
// Compares this object to another object, returning an integer that
// indicates the relationship.
// Returns a value less than zero if this object
// null is considered to be less than any instance.
// If object is not of type Int16, this method throws an ArgumentException.
//
//| <include path='docs/doc[@for="Int16.CompareTo"]/*' />
public int CompareTo(Object value)
{
if (value == null)
{
return 1;
}
if (value is Int16)
{
return m_value - ((Int16)value).m_value;
}
throw new ArgumentException("Arg_MustBeInt16");
}
public int enum_exist_quantify_smart(int s, int[] bounded)
{
if (node(s).type == NodeType.CONSTANT)
return s;
EnumQuantification quant = new EnumQuantification(this);
int r = quant.enum_exist_quantify(s, bounded, false);
return r;
}
public int enum_exist_quantify_dumb(int s, int[] bounded)
{
EnumQuantification quant = new EnumQuantification(this);
int r = quant.enum_exist_quantify_dumb(s, bounded, false);
return r;
}
public int expand_exist_quantify(int s, int[] bounded)
{
int flag = alloc_flag();
mark_transitive_fanins(s, flag);
int result = s;
foreach (int input in bounded)
{
sharp_assert(node(input).is_pi());
int[] orig = { input };
int[] replace = { zero() };
int cofactor_i = compose(result, orig, replace);
replace = new int[] { one() };
int cofactor_ip = compose(result, orig, replace);
result = bor(cofactor_i, cofactor_ip);
}
free_flag(flag);
return result;
}
//| <include path='docs/doc[@for="Int16.Equals"]/*' />
public override bool Equals(Object obj)
{
if (!(obj is Int16))
{
return false;
}
return m_value == ((Int16)obj).m_value;
}
// Returns a HashCode for the Int16
//| <include path='docs/doc[@for="Int16.GetHashCode"]/*' />
public override int GetHashCode()
{
return ((int)((ushort)m_value) | (((int)m_value) << 16));
}
//| <include path='docs/doc[@for="Int16.ToString"]/*' />
public override String ToString()
{
return ToString(null);
}
//| <include path='docs/doc[@for="Int16.ToString2"]/*' />
public String ToString(String format)
{
if (m_value < 0 && format != null && format.Length > 0 && (format[0] == 'X' || format[0] == 'x'))
{
uint temp = (uint)(m_value & 0x0000FFFF);
return Number.FormatUInt32(temp, format);
}
return Number.FormatInt32(m_value, format);
}
//| <include path='docs/doc[@for="Int16.Parse"]/*' />
public static short Parse(String s)
{
return Parse(s, NumberStyles.Integer);
}
//| <include path='docs/doc[@for="Int16.Parse3"]/*' />
public static short Parse(String s, NumberStyles style)
{
NumberFormatInfo.ValidateParseStyle(style);
int i = Number.ParseInt32(s, style);
// We need this check here since we don't allow signs to specified in hex numbers. So we fixup the result
// for negative numbers
if (((style & NumberStyles.AllowHexSpecifier) != 0) && (i <= UInt16.MaxValue)) // We are parsing a hexadecimal number
return (short)i;
if (i < MinValue || i > MaxValue) throw new OverflowException("Overflow_Int16");
return (short)i;
}
private void include_cl_in_reasoning(int cl_id)
{
Clause cl = clause(cl_id);
if (cl.num_lits > 1)
{
int max_idx = -1, max2_idx = -1, max_dl = -1, max2_dl = -1;
for (int i = 0; i < cl.num_lits; ++i)
{
int dl = var_dlevel(cl.literal(i) >> 1);
if (dl < 0 || (lit_value(cl.literal(i)) == 1)) //non-0 variable, so make it the highest possible dl
dl = num_variables() + 1;
if (dl > max_dl)
{
max2_idx = max_idx;
max_idx = i;
max2_dl = max_dl;
max_dl = dl;
}
else if (dl > max2_dl)
{
max2_idx = i;
max2_dl = dl;
}
}
//the invariance: Literal 0 and 1 are watched
int temp = cl.literal(0);
cl.literals[0] = cl.literal(max_idx);
cl.literals[max_idx] = temp;
int svar = cl.literal(0);
watched_by(svar).push_back(cl_id + cl_id);
if (max2_idx == 0)
max2_idx = max_idx;
temp = cl.literal(1);
cl.literals[1] = cl.literal(max2_idx);
cl.literals[max2_idx] = temp;
svar = cl.literal(1);
watched_by(svar).push_back(cl_id + cl_id + 1);
}
}
void remove_cl_from_reasoning(int cl_id)
{
Clause cl = clause(cl_id);
sharp_assert(cl.num_lits > 1);
for (int k = 0; k < 2; ++k)
{ //two watched
int lit = cl.literal(k);
IntVector watch = watched_by(lit);
int i, sz;
for (i = 0, sz = watch.size(); i < sz; ++i)
{
if ((watch[i] >> 1) == cl_id)
{ //found it
watch[i] = watch.back;
watch.pop_back();
break;
}
}
}
}
private void incr_lits_count(int lit)
{
if ((lit & 1) == 1)
++variable(VID(lit)).lits_count_1;
else
++variable(VID(lit)).lits_count_0;
}
private void decr_lits_count(int lit)
{
if ((lit & 1) == 1)
--variable(VID(lit)).lits_count_1;
else
--variable(VID(lit)).lits_count_0;
}
private int get_free_clause_id()
{
int cl_id;
if (!free_clauses.empty())
{
cl_id = free_clauses.back;
free_clauses.pop_back();
clauses[cl_id] = new Clause();
}
else
{
cl_id = clauses.size();
clauses.push_back(new Clause());
}
return cl_id;
}
private int add_clause_to_db(int[] lits, ClType tp, ushort gflag)
{
sharp_assert(lits.Length > 0);
int cl_id = get_free_clause_id();
Clause cl = clause(cl_id);
cl.init(tp, lits, gflag, unique_id++);
// Console.Write("{0} :", cl_id);
// for (int i=0; i< lits.Length; ++i)
// Console.Write ("{0} ", lits[i]);
// Console.WriteLine ("");
for (int i = 0; i < cl.num_lits; ++i)
{
incr_lits_count(cl.literal(i));
reference(cl.literal(i));
}
if (tp == ClType.ORIGINAL)
{
++stats.num_orig_clauses;
original_clauses.push_back(cl_id);
stats.num_orig_literals += lits.Length;
}
else if (tp == ClType.CONFLICT)
{
++stats.num_learned_clauses;
conflict_clauses.push_back(cl_id);
stats.num_learned_literals += lits.Length;
}
include_cl_in_reasoning(cl_id);
return cl_id;
}
internal int add_new_implication(int[] reasons, int implied_lit)
{
if (reasons == null)
{
reasons = new int[dlevel];
for (int i = 0; i < reasons.Length; ++i)
reasons[i] = (assignment_stack(i + 1)[0] ^ 1);
}
for (int i = 0; i < reasons.Length; ++i)
sharp_assert(lit_value(reasons[i]) == 0);
sharp_assert(var_value(VID(implied_lit)) == UNKNOWN);
int cl_id = get_free_clause_id();
Clause cl = clause(cl_id);
int[] lits = new int[1 + reasons.Length];
Array.Copy(reasons, lits, reasons.Length);
lits[reasons.Length] = implied_lit;
cl.init(ClType.TEMP, lits, 0, unique_id++);
temporary_clauses.push_back(cl_id);
queue_implication(implied_lit, cl_id, ImpType.CLAUSE);
return cl_id;
}
int create_op_node(NodeType op, int i1, int i2)
{
if (op == NodeType.AND)
{
if (i1 == zero() || i2 == zero() || i1 == NEGATE(i2))
return zero();
if (i1 == one())
return i2;
if (i2 == one())
return i1;
if (i1 == i2)
return i1;
}
else
{
sharp_assert(op == NodeType.XOR);
if (i1 == zero())
return i2;
if (i1 == one())
return NEGATE(i2);
if (i2 == zero())
return i1;
if (i2 == one())
return NEGATE(i1);
if (i1 == i2)
return zero();
if (i1 == NEGATE(i2))
return one();
}
int r = node_hash.lookup(op, i1, i2);
if (r != INVALID)
return r;
r = create_op_node2(op, i1, i2);
return r;
}
//
// IValue implementation
//
//| <include path='docs/doc[@for="Int16.GetTypeCode"]/*' />
[NoHeapAllocation]
public override TypeCode GetTypeCode()
{
return TypeCode.Int16;
}
//
// This is just designed to prevent compiler warnings.
// This field is used from native, but we need to prevent the compiler warnings.
//
public partial class Foo
{
partial void Bar();
}
public partial class Foo
{
partial void Bar()
{
//
// This is for partial test
}
}
#if _DEBUG
private void DontTouchThis() {
m_value = 0;
this is test
}
#endif
#if _DEBUG
#endif
}
}